Model Checking of Concurrency in Cyber-Physical Systems Specified with Interpreted Petri Nets*

Interpreted Petri nets are a convenient specification technique for control part of cyber-physical systems. In contrast to ordinary Petri nets, they also take into account the presence of input and output signals which are used for communication with the environment. Although there are several analysis and verification methods available that allow checking some structural properties of the nets, the behavioral requirements are of great importance too. In concurrent processes some of the tasks can be realized independently from each other. In the paper we show how the output signal values can be easily tracked in concurrent processes, especially for multiple instances of the same process. We propose how to model interpreted Petri nets as simple timed automata in the commonly available Uppaal tool and how to verify the user-defined properties related to the co-occurrence of particular output signals. The obtained results show that the provided methodology allows to check the concurrency of process instances in a fast, user-friendly and efficient way.