Algorithm of Translation of MSC-specified System into Petri Net

We present in this paper the algorithm which performs the translation of MSC’2000 diagrams into Petri net modulo strong bisimulation. The correctness of this algorithm is justified. Here we supplement MSC’2000 standard supplying it with formal definition of MSC element <condition> by means of process algebra. We would mention here that this translation algorithm is the part of the automated verification system which specifies formally and verify designed software or hardware system specified in MSC language, and is presented in [1], and [2].

• Type: Journal
• Year: 2007
• Where: FUIN
• Authors: Sergiy Kryvyy, Lyudmila Matvyeyeva
• Keywords: Algorithm, Formal Definition, FUIN 2007, Modulo Strong Bisimulation