Title

The Development of a Teaching Tool for Place/Transition Petri Net Design, Analysis and Simulation

Abstract

The Petri net formalism is used for the modelling of Discrete Event Dynamic Systems (DEDS). Its straightforward graphical representation and strong mathematical foundation make it suitable for advanced analysis. The expressiveness of place/transition nets, the elemental form of Petri nets, can be extended with time, modularity, and colours (data-types) to meet specific needs. A Petri net instance is a representation of a dynamic system. Requirements, stipulating the desired behaviour of the model, must be translated to logic formulae to verify the correctness of the model. Temporal logic formalisms CTL and LTL enable precise and automated verification and provide a witness path (or counterexample) that clarifies why a formula is accepted (or rejected). This thesis offers an overview of existing design formalisms (Petri net variants) and analysis formalisms (CTL and LTL), both at syntactical and semantical level. Subsequently, we examine the functionality of three existing programs: PIPE, LoLA, and CPN Tools. Based on this research we introduce a new Petri Net Design, Analysis, and Simulation tool (PNDAS). It is intended as teaching tool. It allows to create and modify place/transition nets, analyse them with both CTL and LTL and simulate the proofs, all within the same GUI. The program can also be used headless, for example as translation program for the file formats of the discussed tools or as back-end verifier. Finally, we compare our new tool with the three others. The feature comparison demonstrates that there is no single program that fits all needs. On the other hand, the model checking performance analysis results in a clear winner. LoLA excels thanks to its gradual exploration of the statespace and state-of-the-art optimisations. PNDAS offers no new functionality; all functions provided can be found in existing tools. It is, however, the first tool that groups a set of functions that are particularly useful in a teaching context. Comparing its performance to existing tools shows us that it is usable for small- to medium-sized models, which are expected in a teaching context.

Downloads

The thesis [pdf].
The powerpoint presentation [.pptx].

Mindmap

References

[1] M. A. Marsan, G. Balbo, G. Chiola, G. Conte, S. Donatelli, and G. Franceschi- nis, “An Introduction to Generalized Stochastic Petri Nets,” Microelectronics Reliability, vol. 31, no. 4, pp. 699–725, 1991.
[2] W. Zuberek, “D-timed Petri Nets and Modeling of Timeouts and Protocols,” Trans. Soc. Comp. Simul., vol. 4, no. 4, pp. 331–357, 1987.
[3] W. Zuberek, “Timed Petri Nets Definitions, Properties, and Applications,” Microelectronics Reliability, vol. 31, no. 4, pp. 627 – 644, 1991.
[4] S. Christensen and L. Petrucci, “Modular Analysis of Petri Nets,” The Com- puter Journal, vol. 43, pp. 224–242, 01 2000.
[5] K. Jensen, “Coloured Petri Nets: A High Level Language for System Design and Analysis,” in High-level Petri Nets, pp. 44–119, Springer, 1991.
[6] D. Giannakopoulou and F. Lerda, “From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata,” in International Conference on Formal Techniques for Networked and Distributed Systems, pp. 308–326, Springer, 2002.
[7] P. Gastin and D. Oddoux, “Fast LTL to Büchi Automata Translation,” in International Conference on Computer Aided Verification, pp. 53–65, Springer, 2001.
[8] M. Silva, “On the History of Discrete Event Systems,” Annual Reviews in Control, vol. 45, pp. 213–222, 2018.
[9] W. H. Fleming, Report of the Panel on Future Directions in Control Theory : A Mathematical Perspective. Soc. for Industrial and Applied Math., 1988.
[10] B. Meyers, R. Deshayes, L. Lucio, E. Syriani, H. Vangheluwe, and M. Wim- mer, “ProMoBox: A Framework for Generating Domain-Specific Property Lan- guages,” in International Conference on Software Language Engineering, pp. 1– 20, Springer, 2014.
[11] C. A. Petri, Kommunikation mit Automaten. PhD thesis, Universitt Hamburg, 1962.
[12] R. Zurawski and M. Zhou, “Petri Nets and Industrial Applications: A Tutorial,” IEEE Transactions on industrial electronics, vol. 41, no. 6, pp. 567–583, 1994.
[13] T. Murata, “Petri Nets: Properties, Analysis and Applications,” Proceedings of the IEEE, vol. 77, pp. 541–580, April 1989.
[14] J. L. Peterson, “Petri Nets,” ACM Comput. Surv., vol. 9, pp. 223–252, Sept. 1977.
[15] R. M. Karp and R. E. Miller, “Parallel Program Schemata,” Journal of Com- puter and System Sciences, vol. 3, no. 2, pp. 147–195, 1969.
[16] T. Agerwala, “A Complete Model for Representing the Coordination of Asyn- chronous Processes,” tech. rep., Johns Hopkins Univ., Baltimore, Md.(USA), 1974.
[17] J. Wang, Timed Petri Nets: Theory and Application, vol. 9. Springer Science & Business Media, 2012.
[18] K. Jensen, “A Brief Introduction to Coloured Petri Nets,” in International Workshop on Tools and Algorithms for the Construction and Analysis of Sys- tems, pp. 203–208, Springer, 1997.
[19] M. Y. Vardi, “Branching vs. Linear Time: Final Showdown,” in International Conference on Tools and Algorithms for the Construction and Analysis of Sys- tems, pp. 1–22, Springer, 2001.
[20] G. J. Holzmann, “The model checker spin,” IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279–295, 1997.
[21] L. Lúcio, S. Mustafiz, J. Denil, H. Vangheluwe, and M. Jukss, “FTG+PM: An Integrated Framework for Investigating Model Transformation Chains,” in International SDL Forum, pp. 182–202, Springer, 2013.
[22] B. Vergauwen and J. Lewi, “A linear local model checking algorithm for ctl,” in International Conference on Concurrency Theory, pp. 447–461, Springer, 1993.
[23] K. Heljanko, Model Checking the Branching Time Temporal Logic CTL. Re- search Report A45, Helsinki University of Technology, Digital Systems Labo- ratory, Espoo, Finland, 1997.
[24] D. E. Muller, A. Saoudi, and P. E. Schupp, “Alternating Automata, the Weak Monadic Theory of the Tree, and its Complexity,” in International Colloquium on Automata, Languages, and Programming, pp. 275–283, Springer, 1986.
[25] K. Etessami and G. J. Holzmann, “Optimizing Büchi Automata,” in Interna- tional Conference on Concurrency Theory, pp. 153–168, Springer, 2000.
[26] F. Somenzi and R. Bloem, “Efficient Büchi Automata from LTL Formulae,” in International Conference on Computer Aided Verification, pp. 248–263, Springer, 2000.
[27] R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, “Simple On-the-fly Automatic Verification of Linear Temporal Logic,” in International Conference on Protocol Specification, Testing and Verification, pp. 3–18, Springer, 1995.
[28] M. Daniele, F. Giunchiglia, and M. Y. Vardi, “Improved Automata Generation for Linear Temporal Logic,” in International Conference on Computer Aided Verification, pp. 249–260, Springer, 1999.
[29] C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, “Memory-Efficient Algorithms for the Verification of Temporal Properties,” Formal Methods in System Design, vol. 1, no. 2-3, pp. 275–288, 1992.
[30] J. Geldenhuys and A. Valmari, “More Efficient On-the-fly LTL Verification with Tarjan’s Algorithm,” Theoretical Computer Science, vol. 345, no. 1, pp. 60–82, 2005.
[31] P. Bonet, C. M. Lladó, R. Puijaner, and W. J. Knottenbelt, “PIPE v2. 5: A Petri Net Tool for Performance Modelling,” in Proc. 23rd Latin American Conference on Informatics (CLEI 2007), 2007.
[32] M. Weber and E. Kindler, “The Petri Net Markup Language,” in Petri Net Technology for communication-based systems, pp. 124–144, Springer, 2003.
[33] K. Schmidt, “LoLA a Low Level Analyser,” in Application and Theory of Petri Nets 2000 (M. Nielsen and D. Simpson, eds.), (Berlin, Heidelberg), pp. 465–474, Springer Berlin Heidelberg, 2000.
[34] T. Liebke and K. Wolf, “Taking Some Burden Off an Explicit CTL Model Checker,” in Application and Theory of Petri Nets and Concurrency (S. Do- natelli and S. Haar, eds.), (Cham), pp. 321–341, Springer International Pub- lishing, 2019.
[35] R. Tarjan, “Depth-first Search and Linear Graph Algorithms,” SIAM journal on computing, vol. 1, no. 2, pp. 146–160, 1972.
[36] K. Jensen, L. M. Kristensen, and L. Wells, “Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems,” International Journal on Software Tools for Technology Transfer, vol. 9, no. 3-4, pp. 213–254, 2007.
[37] K. Jensen and L. M. Kristensen, CPN ML Programming, pp. 43–77. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009.
[38] C. Sren and M. K. H., “Design/CPN ASK-CTL Manual.” http://cpntools. org/wp-content/uploads/2018/01/askctlmanual.pdf.
[39] C. S. Jensen Kurt and K. L. M., “CPN Tools State Space Manual.” http: //cpntools.org/wp-content/uploads/2018/01/manual.pdf.
[40] M. Westergaard and L. M. Kristensen, “The Access/CPN Framework: A Tool for Interacting with the CPN Tools Simulator,” in International Conference on Applications and Theory of Petri Nets, pp. 313–322, Springer, 2009.
[41] K. Wolf, “Petri Net Model Checking with LoLA 2,” in International Confer- ence on Applications and Theory of Petri Nets and Concurrency, pp. 351–362, Springer, 2018.
[42] S. Cayir and M. Ucer, “An Algorithm to Compute a Basis of Petri Net In- variants,” in 4th ELECO Int. Conf. on Electrical and Electronics Engineering. UCTEA, Bursa, Turkey, 2005.
[43] The Central Repository for Petri Net Model Checking Contests https:// pnrepository.lip6.fr/.