Journal
INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE
Volume 22, Issue 1, Pages 133-142Publisher
WORLD SCIENTIFIC PUBL CO PTE LTD
DOI: 10.1142/S0129054111007897
Keywords
P systems; Kripke structures; model checking; SPIN; PROMELA; NuSMV
Categories
Funding
- CNCSIS - UEFISCSU [PNII - IDEI 643/2008]
Ask authors/readers for more resources
This paper presents an approach to P system verification using the SPIN model checker. It proposes a P system implementation in PROMELA, the modeling language accepted by SPIN. It also provides the theoretical background for transforming the temporal logic properties expressed for the P system into properties of the executable implementation. Furthermore, a comparison between P systems verification using SPIN and NuSMV is realized. The results obtained show that the PROMELA implementation is more adequate, especially for verifying more complex models, such as P systems that model ecosystems.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available