Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets
- PDF / 213,657 Bytes
- 10 Pages / 594 x 792 pts Page_size
- 58 Downloads / 195 Views
VERIFYING UCM SPECIFICATIONS OF DISTRIBUTED SYSTEMS USING COLORED PETRI NETS1 N. V. Vizovitin,a† V. A. Nepomniaschy,a‡ and A. A. Stenenkoa††
UDC 519.172
Abstract. This article presents a new method for the analysis and verification of Use Case Map (UCM) specifications with the help of colored Petri nets and the SPIN model checker. Standardized UCM notation is a convenient visual language that allows one to formally represent functional requirements. Algorithms for translating UCM specifications into colored Petri nets and colored Petri nets into the input language Promela of the SPIN model checker are described. The complexity of the obtained colored Petri nets is evaluated. The execution of the presented translation algorithms and support tools is illustrated by the example of error localization and correction in the initial UCM specification of a simple network protocol. Keywords: verification, specification, distributed system, Use Case Map notation, colored Petri net, SPIN model checker. INTRODUCTION At early stages of developing software projects such as the collection and analysis of requirements, of great importance is the nonadmission of errors that can lead to serious negative consequences. The graphic notation of Use Case Maps (UCMs) allows one to formally describe and analyze functional requirements and, at the same time, to preserve the possibility of monitoring requirements by customers. UCM specifications have universal character [1]. For example, they are used for the creation of test scenarios [2, 3], test coverage criteria [4], and also as a property specification language [5]. UCM specifications form a set of scenarios as a collection of cause-and-effect relations between actions in a system. Actions can be associated with components of the system and can reflect its architecture. UCM specifications describe interactions between architectural entities with paying attention to cause-and-effect relations and abstracting from some details of messaging and data processing. Note that tools for the analysis and verification of UCM specifications are insufficiently developed. The UCM standard [6] defines the analysis procedure implemented in the jUCMNav editor [7]. However, this analysis technique is primitive and it is difficult to make the best use of it. This standard formally describes abstract and concrete syntaxes together with constraints to correctly represent UCM specifications. But its semantics is informally described using requirements on the traversal of UCM maps. Therefore, the objective of a number of works consists of the description of a formal semantics for UCMs. J. Hassine and his coauthors presented a formal semantics for a subset of UCMs on the basis of abstract automata together with support tools for the simulation of UCM specifications [8]. They also investigated the application of time constraints in UCM specifications with the use of a UCM extension called Timed Use Case Maps [9]. Some semantics based on timed finite-state automata (together with support tools based on the UPP
Data Loading...
