A distributed verification approach for modular Petri nets

ABSTRACT

This paper reviews a proposal for the modular analysis of Petri nets. It improves the modularity of the verification process using modular state spaces. By adding some computations during the construction of the modular state space, one can determine the liveness of a module without exploring other local information. Thereby, it is suitable for the conception of a new distributed verification approach where every site maintains one module. The sites need to cooperate only during the construction of the modular state space.

REFERENCES

• 1: Antti Valmari, Compositional State Space Generation, Papers from the 12th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets 1993, p.427-457, June 01, 1991
• 2: Antti Valmari , Martti Tienari, An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm, Proceedings of the IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XI, p.3-18, June 18-20, 1991
• 3: Soren Christensen and Laure Petrucci. Modular analysis of Petri nets. The Computer Journal, 43(3):224--242, 2000.
• 4: Modular Analysis of Systems Composed of Semiautonomous Subsystems, Proceedings of the Fourth International Conference on Application of Concurrency to System Design, p.185, June 16-18, 2004
• 5: Marko Mäkelä. Model Checking Safety Properties in Modular High-Level Neets. In W. van der Aalst and E. Best, editors, 24th International Conference on the Application and Theory of Petri Nets, volume 2679 of LNCS, pages 201--220, Eindhoven, The Netherlands, 2002. Springer, July 01 2004.
• 6: Gianfranco Ciardo, Distributed and structured analysis approaches to study large and complex systems, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
• 7: Tamir Heyman Orna Grumberg and Assaf Schuster. A work-efficient distributed algorithm for reachability analysis. In CAV: International Conference on Computer Aided Verification, 2003.
• 8: Lars Kristensen and Laure Petrucci. An approach to distributed state space exploration for coloured petri nets. In Proc. 4th Int. Conf. on Application of Concurrency to System Design (ACSD'04), Hamilton, Canda, June 2004, pages 185--194. IEEE Comp. Soc. Press, June 2004.
• 9: Charles Lakos and Laure Petrucci. Distributed and modular state space exploration for timed petri nets. In Workshop on Practical Use of Coloured Petri Nets, Aarhus, Denmark, pages 191--210, October 2005.

INDEX TERMS

Keywords:
Petri net, analysis, distributed, verification