%0 Generic
%D 2012
%T Towards an Integrated Approach for Model Simulation, Property Extraction and Verification of P Systems
%A Raluca Lefticaru
%A Florentin Ipate
%A Luis Valencia-Cabrera
%A Adrian Turcanu
%A Cristina Tudose
%A Marian Gheorghe
%A Mario J. Pérez-Jiménez
%A Ionut M. Niculescu
%A Ciprian Dragomir
%C Seville, Spain
%I Fénix Editora
%P 291-318
%S Proceedings of the Tenth Brainstorming Week on Membrane Computing
%U http://www.gcn.us.es/10BWMC/10BWMCvolI/papers/paper_pit_sev_sheff.pdf
%V I
%X This paper presents an integrated approach for model simulation, property extraction and formal verication 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 veried 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.
%8 02/2012