Towards an integrated approach for model simulation, property extraction and verification of P systems

Raluca Lefticaru; Florentin Ipate; Luis Valencia-Cabrera; Adrian Turcanu; Cristina Tudose; Marian Gheorghe; Mario Pérez-Jiménez; Ionut-Mihai Niculescu; Ciprian Dragomir

Towards an integrated approach for model simulation, property extraction and verification of P systems

Raluca Lefticaru, Florentin Ipate, Luis Valencia-Cabrera, Adrian Turcanu, Cristina Tudose, Marian Gheorghe, Mario Pérez-Jiménez, Ionut-Mihai Niculescu, Ciprian Dragomir

School of Mathematical & Computer Sciences

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

This paper presents an integrated approach for model simulation, property extraction and formal verification of P systems, illustrated on a tissue P system with active membranes solving the 3-colouring problem. The paper focuses on this problem and reports the invariants and the properties extracted and verified using a series of tools (Daikon, MeCoSim, Maple, Spin, ProB) and languages (P-Lingua, Promela, Event-B). Appropriate tools and integration plugins, which facilitate and even automate the steps involved in the aforementioned approach, have also been developed. The case study chosen is complex (it involves an exponential growth of the number of states through the use of membrane division rules) and the properties obtained are non-trivial.

Original language	English
Title of host publication	Proceedings of the Tenth Brainstorming Week on Membrane Computing
Publisher	Fénix Editora
Pages	291-318
Number of pages	28
Volume	1
ISBN (Print)	9788494005657
Publication status	Published - Feb 2012

Access to Document

http://www.gcn.us.es/10BWMC/10BWMCvolI/papers/paper_pit_sev_sheff.pdf

Cite this

Lefticaru, R., Ipate, F., Valencia-Cabrera, L., Turcanu, A., Tudose, C., Gheorghe, M., Pérez-Jiménez, M., Niculescu, I.-M., & Dragomir, C. (2012). Towards an integrated approach for model simulation, property extraction and verification of P systems. In Proceedings of the Tenth Brainstorming Week on Membrane Computing (Vol. 1, pp. 291-318). Fénix Editora. http://www.gcn.us.es/10BWMC/10BWMCvolI/papers/paper_pit_sev_sheff.pdf

@inproceedings{d74a6ffe11044da9bde24137b3262cdd,

title = "Towards an integrated approach for model simulation, property extraction and verification of P systems",

abstract = "This paper presents an integrated approach for model simulation, property extraction and formal verification of P systems, illustrated on a tissue P system with active membranes solving the 3-colouring problem. The paper focuses on this problem and reports the invariants and the properties extracted and verified using a series of tools (Daikon, MeCoSim, Maple, Spin, ProB) and languages (P-Lingua, Promela, Event-B). Appropriate tools and integration plugins, which facilitate and even automate the steps involved in the aforementioned approach, have also been developed. The case study chosen is complex (it involves an exponential growth of the number of states through the use of membrane division rules) and the properties obtained are non-trivial.",

author = "Raluca Lefticaru and Florentin Ipate and Luis Valencia-Cabrera and Adrian Turcanu and Cristina Tudose and Marian Gheorghe and Mario P{\'e}rez-Jim{\'e}nez and Ionut-Mihai Niculescu and Ciprian Dragomir",

year = "2012",

month = feb,

language = "English",

isbn = "9788494005657",

volume = "1",

pages = "291--318",

booktitle = "Proceedings of the Tenth Brainstorming Week on Membrane Computing",

publisher = "F{\'e}nix Editora",

}

Lefticaru, R, Ipate, F, Valencia-Cabrera, L, Turcanu, A, Tudose, C, Gheorghe, M, Pérez-Jiménez, M, Niculescu, I-M & Dragomir, C 2012, Towards an integrated approach for model simulation, property extraction and verification of P systems. in Proceedings of the Tenth Brainstorming Week on Membrane Computing. vol. 1, Fénix Editora, pp. 291-318. <http://www.gcn.us.es/10BWMC/10BWMCvolI/papers/paper_pit_sev_sheff.pdf>

TY - GEN

T1 - Towards an integrated approach for model simulation, property extraction and verification of P systems

AU - Lefticaru, Raluca

AU - Ipate, Florentin

AU - Valencia-Cabrera, Luis

AU - Turcanu, Adrian

AU - Tudose, Cristina

AU - Gheorghe, Marian

AU - Pérez-Jiménez, Mario

AU - Niculescu, Ionut-Mihai

AU - Dragomir, Ciprian

PY - 2012/2

Y1 - 2012/2

N2 - This paper presents an integrated approach for model simulation, property extraction and formal verification of P systems, illustrated on a tissue P system with active membranes solving the 3-colouring problem. The paper focuses on this problem and reports the invariants and the properties extracted and verified using a series of tools (Daikon, MeCoSim, Maple, Spin, ProB) and languages (P-Lingua, Promela, Event-B). Appropriate tools and integration plugins, which facilitate and even automate the steps involved in the aforementioned approach, have also been developed. The case study chosen is complex (it involves an exponential growth of the number of states through the use of membrane division rules) and the properties obtained are non-trivial.

AB - This paper presents an integrated approach for model simulation, property extraction and formal verification of P systems, illustrated on a tissue P system with active membranes solving the 3-colouring problem. The paper focuses on this problem and reports the invariants and the properties extracted and verified using a series of tools (Daikon, MeCoSim, Maple, Spin, ProB) and languages (P-Lingua, Promela, Event-B). Appropriate tools and integration plugins, which facilitate and even automate the steps involved in the aforementioned approach, have also been developed. The case study chosen is complex (it involves an exponential growth of the number of states through the use of membrane division rules) and the properties obtained are non-trivial.

M3 - Conference contribution

SN - 9788494005657

VL - 1

SP - 291

EP - 318

BT - Proceedings of the Tenth Brainstorming Week on Membrane Computing

PB - Fénix Editora

ER -

Towards an integrated approach for model simulation, property extraction and verification of P systems

Abstract

Access to Document

Fingerprint

Cite this