Algorithm of Translation of MSC-specified System into Petri Net

• Autorzy: Kryvyy S. , Matvyeyeva L.
• Języki publikacji: EN

Abstrakty

EN

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 the MSC'2000 standard with the formal definition of the MSC < condition > element by means of process algebra. This translation algorithm is the 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 in [1] and [2].

Słowa kluczowe

EN

algorithm; translation algorithm; Petri net

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 3-4
• Strony: 431--445
• Opis fizyczny: bibliogr. 23 poz., wykr.

Twórcy

autor

Kryvyy S.

autor

Matvyeyeva L.

• Institute of Cybernetics, NASD of Ukrainew, Pr. Glushkowa, 40, Kiev-03187, Ukraine,

Bibliografia

• [1] Kryvyy S., Matvyeyeva L., Lopatina M. Automatic Modeling and Analysis of MSC-specified Systems. Fundamenta Informaticae, Vol.67, N. 1-3, August 2005, pp. 107-120.
• [2] Kryvyy S., Matvyeyeva L., Lopatina M. Automatic Analysis and Verification of MSC-specified Telecommunication System. ICINCO-2004 August (25-28) in Setubal/Portugal. In Proc. of First Intern. Conf. On Informatics in Control, Automation a d Robotics, Vol.2, pp. 402-405.
• [3] Adriaan de Groot, Hooman J., Kordon F., et al. A Survey: Applying FormalMethods to a Software Intensive. In Proc. of the IEEE High-Assurance Systems Engineering Workshop, 2001, pp. 55 - 64.
• [4] Clarke E., Wing J. Formal Methods: State of the Art and Future Directions. CMU Computer Science Technical Message CMU-CS-96-178, August 1996. Published in: ACM Computing Surveys, Vol.28,N.4,1996,pp.626-643.
• [5] Kryvyi S.L.,Matveyeva L.Ye. FormalMethods of Analysis of System Properties. Intern. Journ. "Cybernetics and Systems Analysis", Vol. 39, N. 2, pp. 174-191,March, 2003, Springer New York.
• [6] Kryvyy S., Matvyeyeva L., Lopatina M. Automatic Translation of MSC Diagrams into Petri Nets. Intern. Journal "Information Theories&Applications", Vol.10, N.4, pp.423-430, 2003.
• [7] Kryvyy S., Matvyeyeva L., Lopatina, M. Automatic Transformation of MSC Diagrams into Petri Nets. In Proceedings of SCI-2003, Orlando, USA, 29-31 July 2003, Vol. 5, pp. 140-146.
• [8] Mauw S., Reniers M.A. Thoughts on the meaning of conditions. Experts meeting SG10, St.Petersburg TD9016, ITU-TS, 1995.
• [9] Bergstra, J.A., Klop, J.W. Process Algebra for Synchronous Communication. Inform.&Control, Vol. 60, 1984, pp.109-137.
• [10] Murata T. Petri Nets: Properties, Analysis and Applications. in Proc. of the IEEE, 1989, vol. 77, N 4, pp. 541 - 580.
• [11] ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva, 2000.
• [12] ITU-TS Recommendation Z.120 Annex B: Algebraic semantics of Message Sequence Charts. ITU-TS, Geneva, 1995.
• [13] Mauw S., ReniersM.A. An algebraic semantics ofMessage Sequence Charts. The Computer Journal, Vol.37, N.4, pp.269-277, 1994.
• [14] Kluge O. Time in Message Sequence Charts Specifications and How to Derive Stochastic Petri Nets. In Proc. of the Third International Workshop on Communication Based Systems (CBS3), Berlin, March 2000.
• [15] Heymer S. A Semantic for MSC based on Petri-Net Components. SIIM Technical Message A-00-12, June 2000. Informatik-Berichte Humboldt-Universitat zu Berlin, 2000.
• [16] Kluge O., Padberg J., Ehrig H. Modeling Train Control Systems: From Message Sequence Charts to Petri Nets. In Proc. FORMS 2000, Formale Techniken fur die Eisenbahnsicherung, pp.25-42, Fortschritt-Berichte VDI, Reihe 12, N. 44, VDI Verlag, 2000.
• [17] Grabowski J., Graubmann P., Rudolph E. Towards a Petri Net Based Semantics Definition for Message Sequence Charts. In SDL'93 Using Objects, Proceedings of the 6th SDL Forum, Darmstadt. O.Fergemand and A.Sarma (eds), Elsevier Science Publisher B.V. (1993)
• [18] Esparza J., Melzer S. Verification of Safety Properties Using Integer Programming: Beyond the State Equation. Formal Methods in System Design, N.16, 2000, pp.159-189.
• [19] Churina T., Mashukov M., Nepomniaschy V. Towards verification of SDL specified distributed systems: Coloured Petri nets approach. In Proc. CS&P-2001, pp. 37-48. University of Warsaw, Poland, 2001.
• [20] Pixley C. Formal Verification 2004. EDA Tools Forum, 2004.
• [21] Holzmann G., Smith M. Automating Software Feature Verification. Bell Labs Technical Journal, Vol. 5, 2000, pp. 72-87.
• [22] Mäkelä M. Maria: Modular Reachability Analyser for Algebraic System Nets. ICATPN 2002, LNCS, Vol. 2360, pp. 434-444. J. Esparza and C. Lakos (eds.), Spinger-Verlag Berlin Heidelberg 2002.
• [23] J.-M. Colom and M.Koutny (eds.). Application and Theory of Petri Nets 2001. In Proc. of the 22-nd International Conference, ICATPN 2001, Newcastle upon Tyne, UK, June 25-29, 2001, LNCS, Vol. 2075. Spinger-Verlag 2001.