A general translation from nested Petri nets into PROMELA
Mirtha Lina Fern\'andez Venero, Fl\'avio Soares Corr\^ea da Silva
TL;DR
This paper introduces a comprehensive translation method from nested Petri nets to PROMELA, enabling the use of SPIN model checker for analyzing complex systems modeled by nested Petri nets.
Contribution
It presents a novel general translation approach from nested Petri nets into PROMELA, facilitating automated analysis with SPIN.
Findings
Enables analysis of nested Petri nets using SPIN
Addresses performance limitations in verification
Provides a framework for practical system modeling
Abstract
Nested Petri nets have been applied for modeling interaction protocols, mobility, adaptive systems and interorganizational workflows. However, few results have been reported on the use of automated tools for analyzing the behavior of these nets. In this paper we present a general translation from nested Petri nets into PROMELA and explain how some properties of these nets can be studied using SPIN model checker. Besides, we discuss how to deal with the main limitations that may influence SPIN performance when verifying practical examples.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPetri Nets in System Modeling · Service-Oriented Architecture and Web Services · Distributed systems and fault tolerance