<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>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.</p>
</abstract>

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.

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

International Journal of Applied Mathematics and Computer Science

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

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...

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

Publié en ligne: 30 déc. 2021

Pages: 647 - 657

Reçu: 27 avr. 2021

Accepté: 04 sept. 2021

DOI: https://doi.org/10.34768/amcs-2021-0045

Mots clés
safeness, control part of the cyber-physical system, Petri net, state machine cover, place invariant

© 2021 Marcin Wojnakowski et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

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

Publié en ligne: 30 déc. 2021

Pages: 647 - 657

Reçu: 27 avr. 2021

Accepté: 04 sept. 2021

DOI: https://doi.org/10.34768/amcs-2021-0045

Mots cléssafeness, control part of the cyber-physical system, Petri net, state machine cover, place invariant

© 2021 Marcin Wojnakowski et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Mots clés
safeness, control part of the cyber-physical system, Petri net, state machine cover, place invariant