Checking the accessibility of marking Petri nets by inverting state trees for data transmission protocol

Download article in PDF format

Authors: Markov A. V., Voevoda A. A.

Annotation: The final stage of software design needs analysis, capable to detect possible flaws in the system. One of such a method is to study the system randomly at any selected state in which the model can be functioning. To use this approach, it is obligatory to prove the accessibility of a selected state, which will consist of state space inversion followed by reduction of the network. This operation is straightforward and can be useful for models with complex structures. The inversion is demonstrated by data transmission protocol using the rules proposed in the paper to transform the simple Petri net.

Keywords: petri net analysis of the state space, accessibility, inversion, data transfer protocol