Analysis of safeness in a Petri net-based specification of the control part of cyber-physical systems

The paper proposes an algorithm for safeness verification of a Petri net-based specification of the control part of cyber-physical systems. The method involves a linear algebra technique and is based on the computation of the state machine cover of a Petri net. Contrary to the well-known methods, the presented idea does not require obtaining all sequential components, nor the computation of all reachable states in the system. The efficiency and effectiveness of the proposed method have been verified experimentally with a set of 243 test modules (Petri net-based systems). The results of experiments show high efficiency of the proposed method since a solution has been found even for such nets where popular techniques are not able to analyze the safeness of the system. Finally, the presented algorithm is explained in detail using a real-life case-study example of the control part of a cyber-physical system.