Repositorio de producción científica de la Universidad de Sevilla

Towards Automated Verification of P Systems Using Spin

Opened Access Towards Automated Verification of P Systems Using Spin
Exportar a
Autor: Lefticaru, Raluca
Tudose, Cristina
Ipate, Florentin
Fecha: 2011
Publicado en: Proceedings of the Ninth Brainstorming Week on Membrane Computing, 237-250. Sevilla, E.T.S. de Ingeniería Informática, 31 de enero-4 de febrero, 2011
ISBN/ISSN: 9788461518371
Tipo de documento: Ponencia
Resumen: This paper presents an approach to P systems verification using the Spin model checker. A tool which implements the proposed approach has been developed 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.
Tamaño: 219.9Kb
Formato: PDF


Mostrar el registro completo del ítem

Esta obra está bajo una Licencia Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 Internacional

Este registro aparece en las siguientes colecciones