×

Algorithm of translation of MSC-specified system into Petri net. (English) Zbl 1124.68072

Summary: We present in this paper an algorithm which performs the translation of MSC’2000 diagrams into Petri nets modulo strong bisimulation. The correctness of this algorithm is justified. Here we supplement the MSC’2000 standard with the formal definition of the MSC \(\langle\)condition\(\rangle\) element by means of process algebra. This translation algorithm is part of the automated verification system which formally specifies and verifies a designed software or hardware system specified in the MSC language and is presented by S. Kryvyy, L. Matvyeyeva and M. Lopatina in [Fundam. Inform. 67, No. 1–3, 107–120 (2005; Zbl 1096.68091); “Automatic analysis and verification of MSC-specified telecommunication system”, in: Proc. First Int. Conf. Informatics in Control, Automation and Robotics 2, 402–405 (2004)].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

process algebra

Citations:

Zbl 1096.68091

Software:

Maria
PDFBibTeX XMLCite