1. Proceedings
  2. I3M
  3. 2021
  4. EMSS
  5. 10.46354/i3m.2021.emss.044

Developing a Bridge from GPenSIM to NuSMV for Model Checking

  • a Albana Roci ,
  • b Reggie Davidrajuh
  • a,b University of Stavanger, Stavanger, Norway
Cite as
Roci A., Davidrajuh R. (2021). Developing a Bridge from GPenSIM to NuSMV for
Model Checking. Proceedings of the 33rd European Modeling & Simulation Symposium (EMSS 2021), pp. 320-326. DOI: https://doi.org/10.46354/i3m.2021.emss.044

Abstract

The general-purpose Petri Nets Simulator (GPenSIM) is an extensible, easy to use, and flexible Petri Nets modeling tool. It is used to model, simulate and evaluate the performance of discrete event systems. Nevertheless, GPenSIM does not support the formal verification of the nets. The new symbolic model checker (NuSMV) is a state-of-art model checking tool that automatically examines whether a finite transition system (TS) satisfies the property specification under consideration. This paper introduces an algorithm that implicitly utilizes NuSMV in GPenSIM. The algorithm automatically converts the static safe Petri Nets model generated by GPenSIM to the NuSMV description language.

References

  1. Baier, C. and Katoen, J.-P. (2008). Principles of Model Checking. MIT PRESS. 
  2. Ben-Ari, M. (2008). Principles of the spin model checker. Springer-Verlag London. 
  3. Berthomieu, B., Ribet, P., and Vernadat, F. (2004). The tool tina – construction of abstract state spaces for
    petri nets and time petri nets. International Journal of Production Research, 42:2741–2756.
  4. Biere, A., Cimatti, A., Clarke, E., and Zhu, Y. (1999). Symbolic model checking without bdds. Cleaveland 
  5. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., and Tac chella, A. (September 2002). Nusmv 2: An open source tool for symbolic model checking. Brinksma E., Larsen K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, 2402. 
  6. Davidrajuh, R. (2018). Modeling discrete-event systems with gpensim: An introduction. Springer. 
  7. Danelutto M. and Torquati M, 2014. Loop parallelism: a new skeleton perspective on data parallel patterns. Parallel Distributed and Network-based Processing, Torino, Italy
  8. Davidrajuh, R., Skolud, B., and Krenczyk, D. (2020). Incorporating automatic model checking into gpen sim. Modelling and Performance Analysis of Cyclic Sys tems, pages 175–187. 
  9. Grahlmann, B. and Best, E. (1996). Pep — more than a petri net tool. Lecture Notes in Computer Science, 1055. Huth, M. and Ryan, M. (2017). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, United Kindom. 
  10. Jensen, K. and Kristensen, L. (2009). Coloured Petri Nets — Modeling and Validation of Concurrent Systems. Springer-Verlag, Berlin. 
  11. J.R.Burch, E.M.Clarke, and McMillan, K. (June 1992). Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170. 
  12. Jyothi, S. D. (2012). Scheduling flexible manufactur ing system using Petri-nets and genetic algorithm. Department of Aerospace Engineering, Indian Institute of Space Science and Technology: Thiruvananthapuram, In dia. 
  13. Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of IEEE, 77:541–580. Mutarraf, U., Barkaoui, K., Li, Z., Wu, N., and Qu, T. (2018). Transformation of business process model and notation models onto Petri nets and their analy sis. Advances in Mechanical Engineering, 10(12):1 – 21. Nakahori, K. and Yamaguchi, S. (2017). A support tool to design iot services with nusmv. IEEE International Conference on Consumer Electronics (ICCE). 
  14. NuSMV. Nusmv: a new symbolic model checker. Tech nical report. 
  15. Penczek, W. and Półrola, A. (2004). Specification and model checking of temporal properties in time petri nets and timed automata. Applications and Theory of Petri Nets 2004, 3099. 
  16. Peterson, J. (1981). Petri Net Theory and the Modeling of Systems. Prentice-Hall, NJ, USA. 
  17. Reisig, W. (2013). Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Springer-
    Verlag Berlin Heidelberg, Germany. 
  18. Skolud, B., Krenczyk, D., and Davidrajuh, R. (2016).  Solving repetitive production planning problems. 
    an approach based on activity-oriented Petri nets.  In International Joint Conference SOCO’16-CISIS’16- 
    ICEUTE’16, pages 397–407. Springe
  19. Szpyrka, M., Biernacka, A., and Biernacki, J. (2014).  Methods of translation of petri nets to nusmv lan  guage. 
    inia.edu/fasta_www2/fasta_list2.shtml
  20. The complete code (2021). The converter from gpensim 
    to nusmv. Technical report. 
  21. Varpaaniemi, K., Heljanko, K., and Lilius, J. (1997).  Prod 3.2 an advanced tool for efficient reachability 
    analysis. Application and Theory of Petri Nets and Con  currency, PETRI NETS 2018, 1254.
  22. Wolf, K. (2018). Petri net model checking with lola2. Application and Theory of Petri Nets and Concurrency, 
    PETRI NETS 2018, 10877.