Model Checking Based Test Generation from P Systems Using P-Lingua
作者： Florentin Ipate , Raluca Lefticaru , Marian Gheorghe
DOI:
关键词: Nondeterministic algorithm 、 Transformation (function) 、 Specification language 、 Model checking 、 P system 、 Temporal logic 、 Field (computer science) 、 Computer science 、 Programming language 、 Kripke structure
摘要: This paper presents an approach for P system testing, that uses model-checking automatic test generation and P-Lingua as specification language. is based on a transformation of the transitional, nondeterministic, cell-like into Kripke structure, which further used generation, by adding convenient temporal logic specifications. extends our previous work in this field to multi-membrane, transitional system, having cooperative rules, communication between membranes membrane dissolution. A tool, takes input specified translates it language accepted model checker NuSMV has been developed case generation. Some hints regarding using are also given.
unirioja.es
us.es参考文章(23)
Gheorghe Paun, Arto Salomaa, Grzegorz Rozenberg, The Oxford Handbook of Membrane Computing ,(2010)
Zhe Dang, Oscar H. Ibarra, Cheng Li, Gaoyan Xie, On the decidability of model-checking for P systems Journal of Automata, Languages and Combinatorics. ,vol. 11, pp. 279- 298 ,(2006)
Manuel García-Quismondo, Rosa Gutiérrez-Escudero, Ignacio Pérez-Hurtado, Mario J. Pérez-Jiménez, Agustín Riscos-Núñez, An overview of p-lingua 2.0 international conference on membrane computing. pp. 264- 288 ,(2009) , 10.1007/978-3-642-11467-0_20
Edmund M. Clarke, E. Allen Emerson, DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC 25 Years of Model Checking. ,vol. 131, pp. 196- 215 ,(2008) , 10.1007/978-3-540-69850-0_12
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
Mónica Cardona, M. Angels Colomer, Antoni Margalida, Ignacio Pérez-Hurtado, Mario J. Pérez-Jiménez, Delfí Sanuy, A p system based model of an ecosystem of some scavenger birds international conference on membrane computing. pp. 182- 195 ,(2009) , 10.1007/978-3-642-11467-0_14
Marian Gheorghe, Florentin Ipate, On Testing P Systems Membrane Computing. pp. 204- 216 ,(2009) , 10.1007/978-3-540-95885-7_15
Amir Pnueli, The temporal semantics of concurrent programs Theoretical Computer Science. ,vol. 13, pp. 45- 60 ,(1981) , 10.1016/0304-3975(81)90110-9
Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, Marco Roveri, NUSMV: a new symbolic model checker International Journal on Software Tools for Technology Transfer. ,vol. 2, pp. 410- 425 ,(2000) , 10.1007/S100090050046
Miguel A. Martínez-del-Amor, Ignacio Pérez-Hurtado, Mario J. Pérez-Jiménez, Agustín Riscos-Núñez, A P-Lingua based simulator for tissue P systems The Journal of Logic and Algebraic Programming. ,vol. 79, pp. 374- 382 ,(2010) , 10.1016/J.JLAP.2010.03.009