No / Recent research in membrane computing examines and confirms the anticipated modelling potential of kernel P systems in several case studies. On the one hand, this computational model is destined to be an abstract archetype which advocates the unity and integrity of P systems onto a single formalism. On the other hand, this envisaged convergence is conceived at the expense of a vast set of primitives and intricate semantics, an exigent context when considering the development of simulation and verification methodologies and tools. Encouraged and guided by the success and steady progress of similar undertakings, in this paper we directly address the issue of formal verification of kernel P systems by means of model checking and unveil a software framework, kpWorkbench, which integrates a set of related tools in support of our approach. A case study that centres around the well known Subset Sum problem progressively demonstrates each stage of the proposed methodology: expressing a kP system model in recently introduced kP-Lingua; the automatic translation of this model into a Promela (Spin) specification; the assisted, interactive construction of a set of LTL properties based on natural language patterns; and finally, the formal verification of these properties against the converted model, using the Spin model checker.

No / In this short paper one overviews the two years development of kernel P systems (kP systems for short), a basic class of P systems combining features of different variants of such systems. The definition of kP systems is given, some examples illustrate various features of the model and the most significant results are presented.

No / Kernel P systems integrate in a coherent and elegant manner many of the features of different P system variants, successfully used for modelling various applications. In this paper, we present our initial attempt to extend the software framework developed to support kernel P systems: a formal verification tool based on the NuSMV model checker and a large scale simulation environment based on FLAME. The use of these two tools for modelling and analysis of biological systems is illustrated with a synthetic biology example.

No / The paper presents the use of a membrane computing model for specifying a synthetic biology pulse generator example and discusses some simulation results produced by the tools associated with this model and compare their performances. The results show the potential of the simulation approach over the other analysis tools like model checkers.