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.
Top1. Introduction
The relatively new field of Membrane Computing has known a fast development and many applications have been reported (Ciobanu, Păun, & Pérez-Jiménez, 2006), especially in biology and bio-medicine, but also in unexpected directions, such as economics, approximate optimization and computer graphics (Frisco, 2009; Păun, Rozenberg, & Salomaa, 2010). Also, a large number of software tools for simulating P systems have been developed, many of them with the purpose of dealing with real world problems, such as those arisen from biology (Cardona, Colomer, Margalida, Pérez-Hurtado, Pérez-Jiménez, & Sanuy, 2010). Similarly to other nature inspired computing models or evolutionary strategies, P systems have been employed to tackle computationally hard problems (Păun, 2001; Pérez-Jiménez & Riscos-Núñez, 2005). An overview of the state of the art in P system software can be found in Păun, Rozenberg, and Salomaa (2010), chapter 17. The P-Lingua framework, one of the most promising software projects in membrane computing, proposes a new programming language, aiming to become a standard for the representation and simulation of P systems (García-Quismondo, Gutiérrez-Escudero, Martínez-del-Amor, Orejuela-Pinedo, & Pérez-Hurtado, 2009; Martínez-del-Amor, Pérez-Hurtado, Pérez-Jiménez, & Riscos-Núñez, 2010).
After designing a P system that aims to solve a given problem, a validation is needed to ensure that the proposed model corresponds to what it is expected. Automated tools, such as model checkers, would be very useful to prove or disprove ‘on-the-fly’ that the P system meets the expected specification. Model checking is an automated technique for verifying if a model meets a given specification (Clarke, Grumberg, & Peled, 1999). It has been applied for verifying models of hardware and software designs, such as sequential circuits designs, communication protocols, concurrent systems, etc. A model checker is a tool that receives as input a property expressed as a temporal logic formula and a model of the system, given as an operational specification, and verifies, through the entire state space, whether the property holds or not. If a property violation is discovered then a counterexample is returned, that details why the model does not satisfy the property specified. Two widely used temporal specification languages in model checking are Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) (Clarke, Grumberg, & Peled, 1999). Spin is probably the most well-known LTL model checker (Holzmann, 2003; Ben-Ari, 2005). It was written by Gerard Holzmann in the ’80, developed over three decades at Bell Laboratories and it received in 2001 the prestigious ACM System Software Award. The transition systems accepted by SPIN (Simple Promela INterpreter) are described in the modelling language Promela (Process Meta Language) and the LTL formulas are checked using the algorithm advocated in Gerth, Peled, Vardi, and Wolper (1995).
In this paper we present an approach to automatic translation of P systems into executable specifications in Promela, the language accepted by the Spin model checker, and their formal verification using Spin. The paper intends to realize a bridge between P-Lingua, a very promising framework for defining and simulating P systems, and Spin, one of the most successful model checkers. The tool presented in the paper assists in designing and verifying P systems by automatically transforming the P-Lingua specifications into Promela. The properties expected for the P system are specified in a ‘natural language’, using a user-friendly interface, then are automatically translated into LTL specifications for the Promela model; furthermore, the Spin model checker is run against them. In case a counterexample is received, the Spin trace is decoded and expressed in terms of a P system derivation.