Formal Verification of a Subset of UML Diagrams: An Approach Using Maude

Formal Verification of a Subset of UML Diagrams: An Approach Using Maude

Allaoua Chaoui, Okba Tibermacine, Amer R. Zerek
Copyright: © 2011 |Pages: 11
DOI: 10.4018/978-1-61520-789-3.ch002
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

We introduce an approach that deals with the verification of UML collaboration and sequence diagrams in respect to the objects internal behaviors which are commonly represented by state machine diagrams. The approach is based on the translation of theses diagrams to Maude specifications. In fact, Maude is a declarative programming language, an executable formal specification language, and also a formal verification system, which permit the achievement of the approach goals. We define in details the rules of translating UML diagrams elements into their corresponding Maude specifications. We present the algebraic structures that represent the OR-States and the AND-states in a state machine diagram, and the structure that represents the collaboration and the sequence diagrams. Also, we explain the mechanism of the execution and the verification of the translated specification, which is based on rewriting logics rules.
Chapter Preview
Top

Uml Class, State Machine, And Collaboration Diagrams

The basic element for modeling oriented object systems is the active object. An active object has its own thread of control and runs in concurrency with other active objects. A UML class diagram may represent classes of active objects and associations between them.

In this paper we use a simple model of an Automatic Teller Machine (ATM), as it’s represented in (Knapp, 2002). Figure 1 shows a class diagram that specifies two active classes ATM and Bank. The association between the two classes rely an instance of Bank to an instance of ATM, and vice versa. Classes define attributes, operations and signals that may be invoked on instances by call or receive actions.

Figure 1.

Class diagram

978-1-61520-789-3.ch002.f01

The UML class diagrams show a static view of the model. We can associate a UML state machine for each class to define model-objects behaviors. The UML state machine is a variant of classical Harel Statecharts (Dong, 2001). It extends the finite automata by adding hierarchy, concurrent and communication aspects to the automaton. UML state machine depicts the behavior and internal states of an object during its life cycle. As it plays a crucial role in software analysis and modeling.

Complete Chapter List

Search this Book:
Reset