Exploring the properties of MSC documents by translating them into Petri nets
- PDF / 301,946 Bytes
- 7 Pages / 595.276 x 793.701 pts Page_size
- 88 Downloads / 158 Views
EXPLORING THE PROPERTIES OF MSC DOCUMENTS BY TRANSLATING THEM INTO PETRI NETS1 S. L. Kryvyi,a O. V. Chugayenko, b† and L. E. Matveevab‡
UDC 51.681.3
The paper presents the final version of the algorithm for translating MSC-2000 documents to event-equivalent Petri nets. The input document may include any elements of the MSC-2000 language, assuming that condition element value is not used and sequential composition of MSC diagrams is regarded as strict. The algorithm is implemented as a full-functional prototype and can be used to verify software systems. Keywords: Petri nets, MSC, verification. INTRODUCTION Formal methods are widely used for the formal specification, analysis, and verification of software and hardware systems. The essence of formal methods is to automate the verification of systems. As a result, other quality control methods such as testing, code checking, and code static analysis are supplemented and it becomes possible to enhance the production quality up to the level unattainable by testing alone. Due to studies in this field, the verification of program systems is treated now as a separate problem. The model checking method, which makes it possible to verify jet systems, develops actively. Specifications are written in a certain formal logic language, whereas the system is a model used to test the feasibility of its specifications. 1. APPROACHES TO THE VERIFICATION OF PROGRAM SYSTEMS Since modern software is complicated, its development (along with the necessity to react promptly to market requirements, rigid constraints on time and resources, and staff turnover) requires various check methods to meet specific needs. It seems expedient in this case to focus efforts on the quality maintenance. The development of software technologies has passed a long way since 1970 when the waterfall model was invented [1]. Since CMM/CMMI [2] appeared, software development quality maintaining systems became widely popular and studies on the development of new program models continued. Recently, agile programming methods have become popular [3, 4]. They are used in incremental and fast development of applications where release terms are decisive. Modern agile approaches need new methods and advanced processes to be developed, in particular, to integrate formal methods. Combining agile approaches and means of computer-aided control enables fast adaptation of the quality control to variations in the business environment. The iterative development, fast prototyping, and the method of rapid releases can be efficiently supplemented with a computer-aided control system. Such a control system allows detecting initially unstable and/or incomplete requirements and at the same time does not increase the duration of iterations. 1
The study was financed by the Ministry of Education and Science of Ukraine within the framework of the joint Ukrainian-Bulgarian project No. 145/23.02.2009 “Development of distributed virtual laboratories based on advanced access methods for sensory systems design” and by the Bulgarian National
Data Loading...
