{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:26:38Z","timestamp":1759638398630},"reference-count":9,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:p> This paper presents an approach to P system verification using the Spin model checker. It proposes a P system implementation in PROMELA, the modeling language accepted by SPIN. It also provides the theoretical background for transforming the temporal logic properties expressed for the P system into properties of the executable implementation. Furthermore, a comparison between P systems verification using SPIN and NUSMV is realized. The results obtained show that the PROMELA implementation is more adequate, especially for verifying more complex models, such as P systems that model ecosystems. <\/jats:p>","DOI":"10.1142\/s0129054111007897","type":"journal-article","created":{"date-parts":[[2011,1,21]],"date-time":"2011-01-21T10:43:19Z","timestamp":1295606599000},"page":"133-142","source":"Crossref","is-referenced-by-count":17,"title":["FORMAL VERIFICATION OF <font>P<\/font> SYSTEMS USING SPIN"],"prefix":"10.1142","volume":"22","author":[{"given":"FLORENTIN","family":"IPATE","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Pitesti, Str. Targu din Vale nr. 1, 110040, Pitesti, Romania"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"RALUCA","family":"LEFTICARU","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Pitesti, Str. Targu din Vale nr. 1, 110040, Pitesti, Romania"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"CRISTINA","family":"TUDOSE","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Pitesti, Str. Targu din Vale nr. 1, 110040, Pitesti, Romania"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf2","volume-title":"Principles of the SPIN Model Checker","author":"Ben-Ari M.","year":"2008"},{"key":"rf3","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"rf4","series-title":"Natural Computing Series","volume-title":"Applications of Membrane Computing","author":"Ciobanu G.","year":"2006"},{"key":"rf5","volume-title":"Model checking","author":"Clarke E. M.","year":"1999"},{"key":"rf6","first-page":"279","volume":"11","author":"Dang Z.","journal-title":"J. Automata, Lang. Combinatorics"},{"key":"rf8","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.007"},{"key":"rf9","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1693"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-56196-2"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11467-0"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054111007897","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T00:54:04Z","timestamp":1565139244000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054111007897"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":9,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1142\/S0129054111007897"],"URL":"https:\/\/doi.org\/10.1142\/s0129054111007897","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]}}}