Инструментальные системы, поддерживающие стохастические сетевые модели

Автор: Быстров А.В., Вирбицкайте И.Б., Ошевская Е.С.

Журнал: Проблемы информатики @problem-info

Рубрика: Прикладные информационные технологии

Статья в выпуске: 2 (63), 2024 года.

Бесплатный доступ

Стохастические сети Петри - мощное средство моделирования параллельных недетерминированных систем с вероятностными характеристиками, применяемое в самых разных областях человеческой деятельности. Они сочетают наглядность графического представления с развитым математическим и алгоритмическим аппаратом анализа, позволяют изучать не только качественные, но и количественные свойства систем, такие как пропускная способность, надежность, время ожидания и т. и. Разработаны и продолжают появляться новые программные инструменты, поддерживающие создание, модификацию и анализ свойств моделей систем на основе различных вариантов стохастических сетей Петри. В данной работе рассматриваются несколько таких инструментов, доступных в сети Интернет и получивших признание пользователей, обсуждаются предоставляемые ими возможности и проводится их сравнение. Основная цель работы - облегчить исследователю и инженеру выбор наиболее подходящего инструмента моделирования и анализа для решения стоящей перед ним задачи.

Еще

Стохастические сети петри, моделирование, анализ производительности, инструментальные системы

Короткий адрес: https://sciup.org/143183456

IDR: 143183456   |   DOI: 10.24412/2073-0667-2024-2-32-57

Список литературы Инструментальные системы, поддерживающие стохастические сетевые модели

  • Reisig W. Petri Nets: An Introduction. V. 4. Springer, 1985. (EATCS Monographs on Theoretical Computer Science), DOI: 10.1007/978-3-642-69968-9.
  • Boyer M., Roux O. On the Compared Expressiveness of Arc, Place and Transition Time Petri Nets // Fundamenta Informaticae. 2008. Jan. V. 88. P. 225–249.
  • Berthomieu B., Diaz M. Modeling and verification of time dependent systems using time Petri nets // IEEE Transactions on Software Engineering. 1991. Mar. V. 17, N 3. P. 259–273. DOI: 10.1109/32.75415.
  • Molloy M. Performance Analysis Using Stochastic Petri Nets // IEEE Trans. Computers. 1982. V. 31, N 9. P. 913–917. DOI: 10.1109/TC.1982.1676110.
  • Vicario E., Sassoli L., Carnevali L. Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems // IEEE Trans. Software Eng. 2009. V. 35, N 5. P. 703–719. DOI: 10.1109/TSE.2009.36.
  • Wang J. Stochastic Timed Petri Nets and Stochastic Petri Nets // Timed Petri Nets: Theory and Application. Boston, MA: Springer US, 1998. P. 125–153. DOI: 10.1007/978-l-4615-5537-7_5.
  • Ajmone Marsan M. et al. An introduction to generalized stochastic Petri nets // Microelectronics Reliability. 1991. Jan. V. 31, N 4. P. 699–725. DOI: 10.1016/0026-2714(91)90010-5.
  • Ajmone Marsan M., Chiola G. On Petri nets with deterministic and exponentially distributed Bring times // Advances in Petri Nets 1987, covers the 7th European Workshop on Applications and Theory of Petri Nets, Oxford, UK, June 1986. V. 266 / ed. by G. Rozenberg. Springer, 1986. P. 132–145. (Lecture Notes in Computer Science), DOI: 10.1007/3-540-18086-9_23.
  • Dugan J. et al. Extended Stochastic Petri Nets: Applications and Analysis // Performance ’84, Proceedings of the Tenth International Symposium on Computer Performance Modelling, Measurement and Evaluation / ed. by E. Gelenbe. North-Holland, 1984. P. 507–519.
  • Ajmone Marsan M. et al. The Effect of Execution Policies on the Semantics and Analysis of Stochastic Petri Nets // IEEE Trans. Software Eng. 1989. V. 15, N 7. P. 832–846. DOI: 10.1109/32.29483.
  • German R., Lindemann C. Analysis of stochastic Petri nets by the method of supplementary variables // Performance Evaluation. 1994. May. V. 20, N 1–3. P. 317–335. DOI: 10.1016/0166-5316(94)90020-5.
  • Тарасюк И. В. Стохастические сети Петри — формализм для моделирования и анализа производительности вычислительных процессов // Системная информатика. Новосибирск, 2004. С. 135–194.
  • German R. Performance analysis of communication systems — modelling with non- Markovian stochastic Petri nets: Modeling with Non-Markovian Stochastic Petri Nets. Wiley, 2000. P. 456.
  • Biagi M. et al. Exploiting Non-deterministic Analysis in the Integration of Transient Solution Techniques for Markov Regenerative Processes // Quantitative Evaluation of Systems. Springer International Publishing, 2017. P. 20–35. DOI: 10.1007/978-3-319-66335-7_2.
  • Martina S. et al. Performance Evaluation of Fischer’s Protocol through SteadyState Analysis of Markov Regenerative Processes // IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS). 09/2016. P. 355–360. DOI: 10.1109/MASCOTS.2016.72.
  • Horvath A. et al. Transient analysis of non-Markovian models using stochastic state classes // Performance Evaluation. 2012. V. 69, N 7/8. P. 315–335. DOI: 10.1016/j.peva.2011.11.002.
  • Amparore E. Stochastic Modelling and Evaluation Using GreatSPN // ACM- SIGMETRICS Performance Evaluation Review. New York, NY, USA, 2022. June. V. 49, N 4. P. 87–91. DOI: 10.1145/3543146.3543165.
  • Amparore E. et al. Years of GreatSPN // Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi on his 70th Birthday / ed. by L. Fiondella, A. Puliafito. Cham: Springer International Publishing, 2016. P. 227–254. DOI: 10.1007/978-3-319-30599-8-9.
  • K. J., Kristensen L. Coloured Petri Nets. Springer Berlin Heidelberg, 2009. DOI: 10.1007/b95112.
  • ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part 2: Transfer Format, International Standard ISO/IEC 15909, February 2011.
  • Kindler E. The Petri Net Markup Language and ISO/IEC 15909-2: Concepts, Status, and Future Directions // Tagungsband Entwurf komplcxcr Automatisierungssysteme EKA. 2006. P. 35–55.
  • Clarke E., Emerson E. Design and synthesis of synchronization skeletons using branching time temporal logic // Logics of Programs / ed. by D. Kozen. Springer Berlin Heidelberg, 1982. P. 52–71.
  • Deharbe D. A Tutorial Introduction to Symbolic Model Checking // Logic for Concurrency and Synchronisation / ed. by R. de Queiroz. Dordrecht: Springer Netherlands, 2003. P. 215–237. DOI: 10.1007/0-306-48088-3_5.
  • Beccuti M., Franceschinis G., Haddad S. Markov Decision Petri Net and Markov Decision Well- Formed Net Formalisms // Petri Nets and Other Models of Concurrency — ICATPN 2007 / ed. by J. Kleijn, A. Yakovlev. Springer Berlin Heidelberg, 2007. P. 43–62. DOI: 10.1007/978-3-540-73094-1 _6.
  • Emerson E., Sistla A. Symmetry and model checking // Formal Methods in System Design. 1996. V. 9, N 1. P. 105–131. DOI: 10.1007/BF00625970.
  • Babar J. et al. GrcatSPN Enhanced with Decision Diagram Data Structures // Applications and Theory of Petri Nets / ed. by J. Lilius, W. Penczek. Springer Berlin Heidelberg, 2010. P. 308–317.
  • Chaki S., Gurfinkel A. BDD-Based Symbolic Model Checking // Handbook of Model Checking / ed. by E. Clarke et al. Springer, 2018. P. 219–245. DOI: 10.1007/978-3-319-10575-8_8.
  • R. R., S. B., Zimmermann A. An Evaluation Framework for Comparative Analysis of Generalized Stochastic Petri Net Simulation Techniques // IEEE Transactions on Systems, Man, and Cybernetics: Systems. 2020. V. 50. P. 2834–2844. DOI: 10.1109/TSMC.2018.2837643.
  • Pernice S. et al. Multiple Sclerosis Disease: A Computational Approach for Investigating Its Drug Interactions // Computational Intelligence Methods for Bioinformatics and Biostatistics / ed. By P. Cazzaniga et al. Cham: Springer International Publishing, 2020. P. 299–308. DOI: 10.1007/978-3-030-63061-4_26.
  • Amparore E., Donatelli S., Landini E. Modelling and Evaluation of a Control Room Application // Application and Theory of Petri Nets and Concurrency / ed. by W. van der Aalst, E. Best. Cham: Springer International Publishing, 2017. P. 243–263.
  • Richard L. Performance Results for the CSMA/CD Protocol Using GrcatSPN // Journal of Systems and Software. 1997. V. 37, N 1. P. 75–90. DOI: 10.1016/S0164-1212(96)00041-6.
  • Amparore E., Donatelli S. GreatTeach: A Tool for Teaching (Stochastic) Petri Nets // Application nd Theory of Petri Nets and Concurrency. Springer International Publishing, 2018. P. 416–425. DOI: 10.1007/978-3-319-91268-4_24.
  • Castagno P. et al. A computational framework for modeling and studying pertussis epidemiology and vaccination // BMC Bioinformatics. 2020. V. 21, N 8. P. 344. DOI: 10.1186/S12859-020-03648-6.
  • The GrcatSPN Framework. [El. Res.]: https://github.com/greatspn/SOURCES. Accessed: 2024-03-15.
  • Paolieri M. et al. The ORIS Tool: Quantitative Evaluation of Non-Markovian Systems // IEEE Trans. Software Eng. 2021. V. 47, N 6. P. 1211–1225. DOI: 10.1109/TSE.2019.2917202.
  • Carnevali L., Paolieri M., Vicario E. The ORIS tool: app, library, and toolkit for quantitative evaluation of non-Markovian systems // ACM SIGMETRICS Performance Evaluation Review. 2022. V. 49, N 4. P. 81–86. DOI: 10.1145/3543146.3543164.
  • Stewart W. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1995. DOI: 10.1515/9780691223384.
  • Carnevali L. et al. Non-Markovian Performability Evaluation of ERTMS/ETCS Level 3 // Computer Performance Engineering - 12th European Workshop, EPEW 2015. V. 9272 / ed. by M. Beltran, W. Knottenbelt, J. Bradley. Cham: Springer, 2015. P. 47–62. (Lecture Notes in Computer Science), DOI: 10.1007/978-3-319-23267-6_4.
  • Biagi M. et al. Model-Based Quantitative Evaluation of Repair Procedures in Gas Distribution Networks // ACM Trans. Cyber Phys. Syst. 2019. V. 3, N 2. 19:1–19:26. DOI: 10.1145/3284037.
  • Carnevali L., Tarani F., Vicario F. Performability Evaluation of Water Distribution Systems During Maintenance Procedures // IEEE Trans. Syst. Man Cybern. Syst. 2020. V. 50, N 5. P. 1704–1720. DOI: 10.1109/TSMC.2017.2783188.
  • Carnevali L. et al. Using the ORIS Tool and the SIRIO Library for Model- Driven Engineering of Quantitative Analytics // Computer Performance Engineering / ed. byK. Gilly, N. Thomas. Cham: Springer International Publishing, 2023. P. 200–215. DOI: 10.1007/978-3-031-25049-l_13.
  • ORIS Tool. [El. Res.]: http://www.oris-tool.org. Accessed: 2024-03-15.
  • ORIS Tool: The Sirio Library. [El. Res.]: https://github.com/oris-tool/sirio. Accessed: 2024-03-15.
  • Heiner M. et al. Snoopy — A Unifying Petri Net Tool // Application and Theory of Petri Nets. PETRI NETS 2012. V. 7347 / ed. by S. Haddad, L. Pomello. Springer Berlin Heidelberg, 2012. P. 398–407. (Lecture Notes in Computer Science), DOI: 10.1007/978-3-642-31131-4_22.
  • David R., Alla H. Discrete, Continuous, and Hybrid Petri Nets. Springer Berlin Heidelberg, 2010. P. 550. DOI: 10.1007/978-3-642-10669-9.
  • Liu F., Heiner M., Gilbert D. Fuzzy Petri nets for modelling of uncertain biological systems // Briefings in Bioinformatics. 2018. Dec. V. 21, N 1. P. 198–210. DOI: 10.1093/bib/bbyll8.
  • Fujita M., McGeer P., Yang J. Multi-Terminal Binary Decision Diagrams: An Efficient DataStructure for Matrix Representation // Form. Methods Syst. Des. USA, 1997. Apr. V. 10, N 2/3. P. 149–169. DOI: 10.1023/A: 1008647823331.
  • Hucka M. et al. Systems Biology Markup Language (SBML) Level 2 Version 5: Structures and Facilities for Model Definitions // Journal of Integrative Bioinformatics. 2015. V. 12. N 2. P. 731–901. DOI: 10.2390/biecoll-jib-2015-271.
  • Heiner M., Schwarick M., Wegener J.-T. Charlie — An Extensible Petri Net Analysis Tool // Application and Theory of Petri Nets and Concurrency / ed. by R. Devillers, A. Valmari. Cham: Springer International Publishing, 2015. P. 200–211. DOI: 10.1007/978-3-319-19488-2_10.
  • Heiner M., Rohr C., Schwarick M. MARGIE — Model Checking and Reachability Analysis Done Efficiently // Application and Theory of Petri Nets and Concurrency / ed. by J.-M. Colom, J. Desel. Springer Berlin Heidelberg, 2013. P. 389–399. DOI: 10.1007/978-3-642-38697-8_21.
  • Baier C. et al. Model Checking Continuous-Time Markov Chains by Transient Analysis // Computer Aided Verification / ed. by E. Emerson, A. Sistla. Springer Berlin Heidelberg, 2000. P. 358–372.
  • Donaldson R., Gilbert D. A Model Checking Approach to the Parameter Estimation of Biochemical Pathways // Computational Methods in Systems Biology / ed. by M. Heiner, A. M. Uhrmacher. Springer Berlin Heidelberg, 2008. P. 269–287.
  • Chodak J., Heiner M. Spike — Reproducible Simulation Experiments with Configuration File Branching // Computational Methods in Systems Biology. Springer International Publishing, 2019. P. 315–321. DOI: 10.1007/978-3-030-31304-3_19.
  • Gilbert D., Donaldson R. A Monte Carlo model checker for probabilistic LTL with numerical constraints: tech. reP. / Bioinformatics Research Centre, University of Glasgow. 01/2008.
  • Gilbert D. et al. Spatial quorum sensing modelling using coloured hybrid Petri nets and simulative model checking // BMC Bioinformatics. 2019. V. 20, supplement 4. DOI: 10.1186/sl2859-019-2690-z.
  • Hcrajy M. et al. Snoopy’s hybrid simulator: a tool to construct and simulate hybrid biological models // BMC Systems Biology. 2017. July. V. 11, N 1. DOI: 10.1186/S12918-017-0449-6.
  • Zimmermann A. Modelling and Performance Evaluation with TimeNET 4.4 // Quantitative Evaluation of Systems - 14th International Conference, QEST 2017. V. 10503 / ed. by N. Bertrand, L. Bortolussi. Springer, 2017. P. 300–303. (Lecture Notes in Computer Science), DOI: 10.1007/978-3-319-66335-7_19.
  • Selic B. Modeling And Analysis Of Realtime And Embedded Systems With Uml And Marte Developing Cyberphysical Systems. Elsevier Science & Technology, 2014. DOI: 10.1016/C2012-0-13536-5.
  • Zimmermann A. et al. Analysis of Safety-Critical Cloud Architectures with MultiTrajectory Simulation // Annual Reliability and Maintainability Symposium (RAMS). 01/2022. P. 1–7. DOI: 10.1109/RAMS51457.2022.9893923.
  • Fedorova A., Beliautsou V., Zimmermann A. Colored Petri Net Modelling and Evaluation of Drone Inspection Methods for Distribution Networks // Sensors. 2022. V. 22, N 9. DOI: 10.3390/s22093418.
  • Dingle N., Knottenbelt W., Suto T. PIPE2: A Tool for the Performance Evaluation of Generalised Stochastic Petri Nets // SIGMETRICS Performance Evaluation Review ACM. New York, NY, USA, 2009. Mar. V. 36, N 4. P. 34–39. DOI: 10.1145/1530873.1530881.
  • Platform Independent Petri Net Editor v4. [El. Res.]: https://sourceforge.net/projects/ pipe2. Accessed: 2024-03-15.
  • PIPE 5. [El. Res.]: https://github.com/sarahtattersall/PIPE. Accessed: 2024-03-15.
Еще
Статья научная