Welcome to the InfoSci Platform
Reference Hub1
Towards Automated Verification of P Systems Using Spin

Towards Automated Verification of P Systems Using Spin

Raluca Lefticaru, Cristina Tudose, Florentin Ipate
Copyright: © 2014 |Pages: 12
ISBN13: 9781466642539|ISBN10: 146664253X|EISBN13: 9781466642546
DOI: 10.4018/978-1-4666-4253-9.ch010
Cite Chapter Cite Chapter

MLA

Lefticaru, Raluca, et al. "Towards Automated Verification of P Systems Using Spin." Natural Computing for Simulation and Knowledge Discovery, edited by Leandro Nunes de Castro, IGI Global, 2014, pp. 159-170. https://doi.org/10.4018/978-1-4666-4253-9.ch010

APA

Lefticaru, R., Tudose, C., & Ipate, F. (2014). Towards Automated Verification of P Systems Using Spin. In L. Nunes de Castro (Ed.), Natural Computing for Simulation and Knowledge Discovery (pp. 159-170). IGI Global. https://doi.org/10.4018/978-1-4666-4253-9.ch010

Chicago

Lefticaru, Raluca, Cristina Tudose, and Florentin Ipate. "Towards Automated Verification of P Systems Using Spin." In Natural Computing for Simulation and Knowledge Discovery, edited by Leandro Nunes de Castro, 159-170. Hershey, PA: IGI Global, 2014. https://doi.org/10.4018/978-1-4666-4253-9.ch010

Export Reference

Mendeley
Favorite

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.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.