Towards Automated Verification of P Systems Using Spin

View Sample PDF

Author(s): Raluca Lefticaru (University of Pitesti, Romania), Cristina Tudose (University of Pitesti, Romania)and Florentin Ipate (University of Pitesti, Romania)
Copyright: 2014
Pages: 12
Source title: Natural Computing for Simulation and Knowledge Discovery
Source Author(s)/Editor(s): Leandro Nunes de Castro (Mackenzie University, Brazil)
DOI: 10.4018/978-1-4666-4253-9.ch010

Keywords: Biologically-Inspired Computing / Biotechnology and Bioinformatics / Engineering Science Reference / Medicine & Healthcare

Purchase

View Towards Automated Verification of P Systems Using Spin on the publisher's website for pricing and purchasing information.

Abstract

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.

The IRMA Community

Research IRM

Towards Automated Verification of P Systems Using Spin

Purchase

Abstract

Related Content

IRMA Sponsors