{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T14:51:42Z","timestamp":1781103102834,"version":"3.54.1"},"reference-count":25,"publisher":"IGI Global Scientific Publishing","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,7,1]]},"abstract":"<p>This paper presents an approach to P systems verification using the Spin model checker. The authors have developed a tool which implements the proposed approach and can automatically transform P system specifications from P-Lingua into Promela, the language accepted by the well known model checker Spin. The properties expected for the P system are specified using some patterns, representing high level descriptions of frequently asked questions, formulated in natural language. These properties are automatically translated into LTL specifications for the Promela model and the Spin model checker is run against them. In case a counterexample is received, the Spin trace is decoded and expressed as a P system computation. The tool has been tested on a number of examples and the results obtained are presented in the paper.<\/p>","DOI":"10.4018\/jncr.2011070101","type":"journal-article","created":{"date-parts":[[2011,10,19]],"date-time":"2011-10-19T12:42:31Z","timestamp":1319028151000},"page":"1-12","source":"Crossref","is-referenced-by-count":4,"title":["Towards Automated Verification of P Systems Using Spin"],"prefix":"10.4018","volume":"2","author":[{"given":"Raluca","family":"Lefticaru","sequence":"first","affiliation":[{"name":"University of Pitesti, Romania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cristina","family":"Tudose","sequence":"additional","affiliation":[{"name":"University of Pitesti, Romania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florentin","family":"Ipate","sequence":"additional","affiliation":[{"name":"University of Pitesti, Romania"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"jncr.2011070101-0","doi-asserted-by":"crossref","unstructured":"Andrei, O., Ciobanu, G., & Lucanu, D. (2005). Executable specifications of P systems. In G. Mauri, G. P\u0103un, M. J. P\u00e9rez-Jim\u00e9nez, G. Rozenberg, & A. Salomaa (Eds.), Proceedings of the 5th International Workshop on Membrane Computing (LNCS 3365, pp. 126-145).","DOI":"10.1007\/978-3-540-31837-8_7"},{"key":"jncr.2011070101-1","author":"M.Ben-Ari","year":"2005","journal-title":"Principles of the Spin model checker"},{"key":"jncr.2011070101-2","doi-asserted-by":"crossref","unstructured":"Bernardini, F., Gheorghe, M., Romero-Campero, F. J., & Walkinshaw, N. (2007). A hybrid approach to modeling biological systems. In G. Eleftherakis, P. Kefalas, G. Paun, G. Rozenberg, & A. Salomaa (Eds.), Proceedings of the 8th International Conference on Membrane Computing (LNCS 4860, pp. 138-159).","DOI":"10.1007\/978-3-540-77312-2_9"},{"key":"jncr.2011070101-3","doi-asserted-by":"crossref","unstructured":"Cardona, M., Colomer, M. A., Margalida, A., P\u00e9rez-Hurtado, I., P\u00e9rez-Jim\u00e9nez, M. J., & Sanuy, D. (2010). A P system based model of an ecosystem of some scavenger birds. In G. Paun, M. J. P\u00e9rez-Jim\u00e9nez, A. Riscos-N\u00fa\u00f1ez, G. Rozenberg, & A. Salomaa (Eds.), Proceedings of the 10th International Workshop on Membrane Computing (LNCS 5957, pp. 182-195).","DOI":"10.1007\/978-3-642-11467-0_14"},{"key":"jncr.2011070101-4","author":"G.Ciobanu","year":"2006","journal-title":"Applications of membrane computing"},{"key":"jncr.2011070101-5","author":"E. M.Clarke","year":"1999","journal-title":"Model checking"},{"key":"jncr.2011070101-6","doi-asserted-by":"crossref","unstructured":"Dang, Z., Ibarra, O. H., Li, C., & Xie, G. (2005). On model-checking of P systems. In C. S. Calude, M. J. Dinneen, G. Paun, M. J. P\u00e9rez-J\u00edmenez, & G. Rozenberg (Eds.), Proceedings of the 4th International Conference on Unconventional Computation (LNCS 3699, pp. 82-93).","DOI":"10.1007\/11560319_9"},{"issue":"3","key":"jncr.2011070101-7","first-page":"279","article-title":"On the decidability of model-checking for P systems. Journal of Automata","volume":"11","author":"Z.Dang","year":"2006","journal-title":"Languages and Combinatorics"},{"key":"jncr.2011070101-8","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199542864.001.0001"},{"issue":"3","key":"jncr.2011070101-9","doi-asserted-by":"crossref","first-page":"234","DOI":"10.15837\/ijccc.2009.3.2431","article-title":"P-Lingua 2.0: A software framework for cell-like P systems.","volume":"4","author":"M.Garc\u00eda-Quismondo","year":"2009","journal-title":"International Journal of Computers, Communications & Control"},{"key":"jncr.2011070101-10","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M. Y., & Wolper, P. (1995). Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of the International Symposium on Protocol Specification Testing and Verification (pp. 3-18).","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"jncr.2011070101-11","doi-asserted-by":"crossref","unstructured":"Gheorghe, M., Ipate, F., Lefticaru, R., & Dragomir, C. (2011). An integrated approach to P systems formal verification. In M. Gheorghe, T. Hinze, G. Paun, G. Rozenberg, & A. Salomaa (Eds.), Proceedings of the 11th International Workshop on Membrane Computing (LNCS 6501, pp. 226-239).","DOI":"10.1007\/978-3-642-18123-8_18"},{"key":"jncr.2011070101-12","author":"G.Holzmann","year":"2003","journal-title":"The spin model checker: Primer and reference manual"},{"key":"jncr.2011070101-13","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.007"},{"key":"jncr.2011070101-14","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054111007897"},{"key":"jncr.2011070101-15","unstructured":"Ipate, F., & \u0162urcanu, A. (2011). Modelling, verification and testing of P systems using Rodin and ProB. In Proceedings of the Ninth Brainstorming Week on Membrane Computing (pp. 209-220)."},{"issue":"2","key":"jncr.2011070101-16","first-page":"153","article-title":"Model checking based test generation from P systems using P-lingua.","volume":"13","author":"R.Lefticaru","year":"2010","journal-title":"Romanian Journal of Information Science and Technology"},{"key":"jncr.2011070101-17","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.009"},{"key":"jncr.2011070101-18","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1693"},{"issue":"1","key":"jncr.2011070101-19","first-page":"75","article-title":"P systems with active membranes: Attacking NP-complete problems. Journal of Automata","volume":"6","author":"G.P\u0103un","year":"2001","journal-title":"Languages and Combinatorics"},{"key":"jncr.2011070101-20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-56196-2","author":"G.P\u0103un","year":"2002","journal-title":"Membrane computing: An introduction"},{"key":"jncr.2011070101-21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-11467-0","author":"G.P\u0103un","year":"2010","journal-title":"The Oxford handbook of membrane computing"},{"key":"jncr.2011070101-22","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037637"},{"key":"jncr.2011070101-23","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (1977). The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (pp. 46-57).","DOI":"10.1109\/SFCS.1977.32"},{"key":"jncr.2011070101-24","doi-asserted-by":"crossref","unstructured":"Romero-Campero, F. J., Gheorghe, M., Bianco, L., Pescini, D., P\u00e9rez-Jim\u00e9nez, M. J., & Ceterchi, R. (2006). Towards probabilistic model checking on P systems using PRISM. In H. J. Hoogeboom, G. Paun, G. Rozenberg, & A. Salomaa (Eds.), Proceedings of the 7th International Workshop on Membrane Computing (LNCS 4361, pp. 477-495).","DOI":"10.1007\/11963516_30"}],"container-title":["International Journal of Natural Computing Research"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=58062","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T16:29:42Z","timestamp":1654100982000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/jncr.2011070101"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2011,7,1]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,7]]}},"URL":"https:\/\/doi.org\/10.4018\/jncr.2011070101","relation":{},"ISSN":["1947-928X","1947-9298"],"issn-type":[{"value":"1947-928X","type":"print"},{"value":"1947-9298","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7,1]]}}}