Automatic Modeling and Analysis of MSC-specified Systems

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

Abstrakty

EN

Formal Methods are a set of methods and tools based on mathematical modeling and formal logic that are used to specify and verify requirements and architecture of hardware or software systems. They can also include means of automatic proving of key properties of designed software or hardware systems. In this paper automatic system is presented which specifies formally and verify designed software or hardware system specified in MSC language. Automatic system is represented as technological process that applies the formal modeling technique of Petri nets and is based on linear algebra methods of analysis, namely, solving the systems of linear equations over the set of natural numbers, in order to research the properties of a system under design. The system is first modeled as a Petri net, and then this model is analyzed. The understanding of the system which results from the analysis will lead to a hopefully errorless system.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 67, nr 1-3
• Strony: 107--120
• Opis fizyczny: Bibliogr. 23 poz., wykr.

Twórcy

autor

Kryvyy S.

• Politechnical Institute of Rzeszow Str. Pola, 2, Rzeszow, 35-959, Poland

autor

Matvyeyeva L.

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

autor

Lopatina M.

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

Bibliografia

• [1] Wing, J.M. A specifier’s introduction to formal methods. IEEE Computer. - September. - 1990.- P. 8-24.
• [2] Miller S.P., Srivas, M. Formal Verification of the AAMP5 Microprocessor - A Case Study in the Industrial Use of Formal Methods. In Proceedings of the 1995 Workshop on Industrial-Strength Formal Specification Techniques (WIFT’95), IEEE Computer Society, Orlando, Florida, USA, April 5-8, 1995.
• [3] Bolongesi T., Brinksma E. Introduction to ISO specification language LOTOS. Computer Networks and ISDN Systems, Vol. 14. - 1987. -P. 25-59.
• [4] ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva. - 2000.
• [5] Saracco R., Tilanus A.J. CCITT SDL: Overview of the language and its applications. Computer Networks and ISDN Systems, Vol. 14. = 1987. -P. 65-74.
• [6] Jensen, K. EACTS Colored Petri Nets. Vol. 1. Springer-Verlag. - 1992.
• [7] Peterson J. L. Petri Net Theory and the Modeling of Systems. Englewood Cliffs, New Jersey: Prentice-Hall, Inc. 1981.
• [8] Kroger K. EACTS Temporal Logic of Programs. Springer-Verlag. - 1987.
• [9] 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. - P. 140-146
• [10] Bergstra, J.A., Klop, J.W. Process Algebra for Synchronous Communication. Inf. and Control, Vol. 60. - 1984. - P. 109-137.
• [11] Mauw S., Reniers M.A. Thoughts on the meaning of conditions. Experts meeting SG10, St.Petersburg TD9016, ITU-TS. - 1995.
• [12] Krivoi S. A Criteria of compatibility systems of linear diophantine constraints. Lecture Notes in Computer Science. Spring. Verlag. - 2002. - N 2328. - P. 264 – 271.
• [13] Murata T. Petri Nets: Properties, Analysis and Applications. in ”Proceedings of the IEEE, 1989, vol. 77, N 4, P. 541 – 580.
• [14] Esparza J., Melzer S. Verification of Safety Properties Using Integer Programming: Beyond the State Equation. Formal Methods in System Design, N 16. - 2000. - P.159-189.
• [15] McMillan K.L. Using Unfolding to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. In Proc. 4th Workshop on Computer Aided Verification. Lecture Notes in Computer Science, Vol. 663 (1992), 154-174.
• [16] Khomenko V., Kotny M. and Vogler V. Canonical Prefixes of Petri Net Unfoldings. In Proc. of International Conference on Computer Aided Verification (CAV’2002). Lecture Notes in Computer Science, Vol. 240 Springer Verlag (2002) 582-595.
• [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] Kluge O. Time in Message Sequence Charts Specifications and How to Derive Stochastic Petri Nets. In Proceedings of the Third International Workshop on Communication Based Systems (CBS3), Berlin, March 2000.
• [19] Heymer S. A Semantic for MSC based on Petri-Net Components. SIIM Technical Report A-00-12, June 2000. Informatik-Berichte Humboldt-Universitat zu Berlin (2000).
• [20] Kluge O., Padberg J., Ehrig H. Modeling Train Control Systems: From Message Sequence Charts to Petri Nets. Technische Universitat Berlin. Retrieved on April 20, 2001 from http://cs.tu-berlin.de/SPP/index.html
• [21] Bowen T.F., Dworack F.S., Chow C.H., Griffeth N.D., Herman G.E., and Lin Y.J. The feature interaction problem in telecommunications systems. In Proc. 7th Int. Conf. on Software Engineering for Telecommunication Switching Systems, July 1989 (1989) 59-62.
• [22] Cheung T.Y., and Zeng W. Invariant-preserving transformations for the verification of place/transition systems. IEEE Trans. Systems, Man and Cybernetics - Part A, Vol. 28, N 1 (1998) 114-121.
• [23] Nakamura M., Kakuda Y. and Kikuno T. Petri-net based detection method for non-deterministic feature interactions and its experimental evaluation. Feature Interactions in Telecommunication Networks IV. IOS Press (1997) 138-152.