CPN Tools-Assisted Simulation and Verification of Nested Petri Nets
https://doi.org/10.18255/1818-1015-2012-5-115-130
Abstract
Nested Petri nets (NP-nets) are an extension of Petri net formalism within the “netswithin-nets” approach, when tokens in a marking are Petri nets, which have an autonomous behavior and are synchronized with the system net. The formalism of NP-nets allows modeling multi-level multi-agent systems with dynamic structure in a natural way. Currently, there is no tool for supporting NP-nets simulation and analysis. The paper proposes the translation of NP-nets into Colored Petri nets and the use of CPN Tools as a virtual machine for NP-nets modeling, simulation and automatic verification.
About the Authors
L. W. Dworza´nski
Национальный исследовательский университет “Высшая школа экономики”
Russian Federation
преподаватель
Russian Federation
преподаватель
I. A. Lomazova
Национальный исследовательский университет “Высшая школа экономики”
Russian Federation
Russian Federation
профессор
References
1. Ломазова И. А. Вложенные сети Петри: моделирование и анализ распределенных систем с объектной структурой. М.: Научный Мир, 2004. 208 с.
2. van der Aalst, W.M.P., Stahl C., Westergaard M. Strategies for Modeling Complex Processes Using Colored Petri Nets // ToPNoC V. 2012. LNCS 6900. P. 265–291.
3. Bashkin V.A., Lomazova I.A. Resource Driven Automata Nets // Fundamenta Informaticae. 2011. Vol. 109(3). P. 223–236.
4. Bednarczyk M.A., Bernardinello L., Pawlowski W., Pomello L. Modelling mobility with Petri Hypernets // Recent Trends in Algebraic Development Techniques. 2005. LNCS 3423. P. 28–44.
5. Bocˇanealˇa C. Modeling inteligent systems with level Petri nets // Annals of Dunarea de Jos Year. 2008. Vol. 31(2). P. 31–36.
6. Chang L., He X., Lian J., Shatz S. Applying a Nested Petri Net Modeling Paradigm to Coordination of Sensor Networks with Mobile Agents // Proc. of Workshop on Petri Nets and Distributed Systems, Xian, China. 2008. P. 132–145.
7. Dvoryansky L.V., Lomazova I.A. Compositionality of some behavioral properties for free-choice nested Petri nets. // Proc. Second Workshop “Program Semantics, Specification and Verification: Theory and Application”. Yaroslavl, 2011. P. 27–36.
8. Dworza´nski L. W., Lomazova I.A. On Compositionality of Boundedness and Liveness for Nested Petri Nets // Fundamenta Informaticae. 2012. Vol. 120(3–4).P. 277–295.
9. Hoffmann K., Ehrig H., Mossakowski T. High-level nets with nets and rules as tokens // Proc. ICATPN. 2005. LNCS 3536. P. 268–288.
10. ter Hofstede A.H.M., van der Aalst W.M.P., Adams M., Russell N. Modern Business Process Automation: YAWL and its support environment. Springer, 2010. 676 p.
11. Jensen K., Kristensen L. M. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, 2009. 396 p.
12. Jensen K., Kristensen L.M., Wells L. Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems // International Journal on Software Tools for Technology Transfer. 2007. Vol. 9(3–4). P. 213–254.
13. K¨ohler M., Farwer M. Object nets for mobility // Proc. ICATPN. 2007. LNCS 4546. P. 244–262.
14. K¨ohler-Bussmeier M. Hornets: Nets within nets combined with net algebra // Proc. Applications and Theory of Petri Nets. 2009. LNCS 5606. P. 243–262.
15. Lomazova I. A. Nested Petri nets — a Formalism for Specification and Verification of Multi-Agent Distributed Systems // Fundamenta Informaticae. 2000. Vol. 43(1–4). P. 195–214.
16. Lomazova I. A. Nested Petri Nets: Multi-level and Recursive Systems // Fundamenta Informaticae. 2001. Vol. 47(3–4). P.283–293.
17. Lomazova I. A. Nested Petri Nets for Adaptive Process Modeling // Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. 2008. LNCS 4800. P. 460–474.
18. Mascheroni M., Farina F. Nets-Within-Nets paradigm and grid computing // Transactions on Petri Nets and Other Models of Concurrency V. 2012. LNCS 7347. P. 201–220.
19. Pawlowski W. Petri Hypernets with Constraints // Proc. “Concurrency, Specification and Programming (CS&P 2009)”. 2009. P. 467–479.
20. Valk R. Petri Nets as Token Objects: An Introduction to Elementary Object Nets // Proc. of ICATPN’98. LNCS1420. 1998. P. 1–25. 21. Valk R. Object Petri nets: Using the nets-within-nets paradigm // Lectures on
21. Concurrency and Petri Nets. 2004. LNCS 3098. P. 819–848.
22. CPN Tools Manual: Nondeterministic nets. http://cpntools.org/documentation/tasks/verification/nondeterministic_nets
Review
For citations:
Dworza´nski L.W., Lomazova I.A. CPN Tools-Assisted Simulation and Verification of Nested Petri Nets. Modeling and Analysis of Information Systems. 2012;19(5):115-130. (In Russ.) https://doi.org/10.18255/1818-1015-2012-5-115-130
Views:
1221
Email this article 