Matvyeyeva L. Analysis and verification of MSC-specified system by Means of Petri nets

The technological process is built in this thesis to analyze and verify software or hardware system specified in MSC'2000 language. As a mathematical model the system utilizes ordinary Petri nets. The model checking is based on the use of linear algebra methods. The translation algorithm of MSC'2000 description of the designed system into the Petri nets is built, correctness of this algorithm is proved by means of process algebra. The standardized formal semantics of language MSC'2000 is extended by the formal semantics of the language element <condition>. The algorithms of the verification of the following properties are developed: (structural) boundedness, L3-liveness, reachability, deadlock freedom. Original algorithms of building of S- and T-invariants and search of traps and siphons for asymmetric Petri nets are developed and implemented. The original approach of checking the invariance of the properties of original Petri net model is created in order to resolve the feature interaction problem.