Extending GPenSIM for Model Checking on Petri Nets

Reggie Davidrajuh (University of Stavanger, Norway); Damian Krenczyk (Silesian University of Technology, Poland)

Cyber-physical systems involve hardware and software that are highly interconnected and complex. Unexpected failures in these systems can cause material damages, cost a lot of money and reputation, and can risk human lives too. The definite way of avoiding unexpected failures is to make a model of the system and to perform model checking on it. Petri nets are a highly effective way of modelling discrete-event systems. General-purpose Petri Net Simulator (GPenSIM) is a tool for modelling, simulation, performance evaluation, and control of discrete-event systems. GPenSIM lacks the automatic model checking facility until now. Firstly, this paper explores the potentials of incorporating the model checking functions to GPenSIM. Secondly, three functionalities are identified and proposed for extending GPenSIM for automatic model checking.

Journal: International Journal of Simulation- Systems, Science and Technology- IJSSST V20

Published: Feb 27, 2019

DOI: 10.5013/IJSSST.a.20.01.13