maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-5-115-130mais-61Research ArticleОригинальные статьиArticlesИмитационное моделирование и верификация вложенных сетей Петри с использованием CPNToolsCPN Tools-Assisted Simulation and Verification of Nested Petri NetsДворянскийЛеонид ВладимировичDworza´nskiL. W.

преподаватель

преподаватель

leo@mathtech.ruЛомазоваИрина АлександровнаLomazovaI. A.

профессор

профессор

ilomazova@hse.ruНациональный исследовательский университет “Высшая школа экономики”РоссияНациональный исследовательский университет “Высшая школа экономики”Russian Federation201204032015195115130Copyright © Дворянский Л.В., Ломазова И.А., 20152015Дворянский Л.В., Ломазова И.А.Dworza´nski L.W., Lomazova I.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/61

Вложенные сети Петри (NP-сети) — это расширение сетей Петри в рамках подхода “nets-within-nets”, когда фишки в разметке сети сами являются сетями Петри и обладают автономным поведением, при этом имеются средства синхронизации сетевых фишек и системной сети. Формализм NP-сетей позволяет естественным образом моделировать многоуровневые мультиагентные системы с динамической структурой. В настоящее время не существует инструментальной поддержки имитационного моделирования и анализа вложенных сетей Петри. В работе предлагается проводить имитационное моделирование и построение графа достижимости для NP-сетей путем перевода NP-сетей в раскрашенные сети Петри и использования инструментария CPN Tools в качестве виртуальной машины для исполнения и средства автоматического анализа ис- ходных NP-сетей.

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.

вложенные сети Петрираскрашенные сети Петриимитационное моделированиеверификацияграф достижимостиnested Petri netscolored Petri netssimulationverificationreachability graphНаучный фонд НИУ ВШЭ, РФФИReferencesЛомазова И. А. Вложенные сети Петри: моделирование и анализ распределенных систем с объектной структурой. М.: Научный Мир, 2004. 208 с.Ломазова И. А. Вложенные сети Петри: моделирование и анализ распределенных систем с объектной структурой. М.: Научный Мир, 2004. 208 с.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.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.Bashkin V.A., Lomazova I.A. Resource Driven Automata Nets // Fundamenta Informaticae. 2011. Vol. 109(3). P. 223–236.Bashkin V.A., Lomazova I.A. Resource Driven Automata Nets // Fundamenta Informaticae. 2011. Vol. 109(3). P. 223–236.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.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.Bocˇanealˇa C. Modeling inteligent systems with level Petri nets // Annals of Dunarea de Jos Year. 2008. Vol. 31(2). P. 31–36.Bocˇanealˇa C. Modeling inteligent systems with level Petri nets // Annals of Dunarea de Jos Year. 2008. Vol. 31(2). P. 31–36.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.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.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.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.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.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.Hoffmann K., Ehrig H., Mossakowski T. High-level nets with nets and rules as tokens // Proc. ICATPN. 2005. LNCS 3536. P. 268–288.Hoffmann K., Ehrig H., Mossakowski T. High-level nets with nets and rules as tokens // Proc. ICATPN. 2005. LNCS 3536. P. 268–288.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.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.Jensen K., Kristensen L. M. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, 2009. 396 p.Jensen K., Kristensen L. M. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, 2009. 396 p.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.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.K¨ohler M., Farwer M. Object nets for mobility // Proc. ICATPN. 2007. LNCS 4546. P. 244–262.K¨ohler M., Farwer M. Object nets for mobility // Proc. ICATPN. 2007. LNCS 4546. P. 244–262.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.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.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.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.Lomazova I. A. Nested Petri Nets: Multi-level and Recursive Systems // Fundamenta Informaticae. 2001. Vol. 47(3–4). P.283–293.Lomazova I. A. Nested Petri Nets: Multi-level and Recursive Systems // Fundamenta Informaticae. 2001. Vol. 47(3–4). P.283–293.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.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.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.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.Pawlowski W. Petri Hypernets with Constraints // Proc. “Concurrency, Specification and Programming (CS&P 2009)”. 2009. P. 467–479.Pawlowski W. Petri Hypernets with Constraints // Proc. “Concurrency, Specification and Programming (CS&P 2009)”. 2009. P. 467–479.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 onValk 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 onConcurrency and Petri Nets. 2004. LNCS 3098. P. 819–848.Concurrency and Petri Nets. 2004. LNCS 3098. P. 819–848.CPN Tools Manual: Nondeterministic nets. http://cpntools.org/documentation/tasks/verification/nondeterministic_netsCPN Tools Manual: Nondeterministic nets. http://cpntools.org/documentation/tasks/verification/nondeterministic_nets

The authors declare that there are no conflicts of interest present.