摘要 : 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 trans... 展开 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. 收起