Automatic Model Checking of State Machines

A seminar report submitted to MANIPAL UNIVERSITY

For Partial Fulfillment of the Requirement for the Award of the Degree of Master of Technology in Software Engineering by Anusha A Reg. No. 130928001

February 2014

Abstract The idea of Model Driven Development (MDD) is to specify requirements of systems in a formal (usually graphical) notation. UML is the initial and dominant modelling phase in software engineering arena. If errors are occurring in this phase of software development itself, it will cost a lot. Hence it is crucial to detect model level errors in the initial phase rather than later stages of software development. An approach to automatically verifying models composed of UML state machines. This approach helps in checking safety/liveness, properties, trace refinement, relationships and so on with the help of PAT (Process Analysis Toolkit) and CSP (communicating sequential programs).

1

1
1.1

Introduction
State Machines

The concepts behind state machines are about organizing the way a device, computer program, or other (often technical) process works such that an entity or each of its sub-entities is always in exactly one of a number of possible states and where there are well-defined conditional transitions between these states. The UML state diagrams are directed graphs in which nodes denote states and connectors denote state transitions. In UML, states are represented as rounded rectangles labeled with state names. The transitions, represented as arrows, are labeled with the triggering events followed optionally by the list of executed actions. 1.1.1 UML State Machine Components

Figure 1: State Machine.

As in Fig. 1, the initial transition originates from the solid circle and specifies the default state when the system first begins. An event is something that happens that affects the system A state captures the relevant aspects of the system’s history very efficiently. Guard conditions are Boolean expressions evaluated dynamically based on the value of extended state variables and event parameters. Guard conditions affect the behavior of a state machine by enabling actions or transitions only when they evaluate to TRUE and disabling them when they evaluate to FALSE. When an event instance is 2

dispatched, the state machine responds by performing actions Switching from one state to another is called state transition, and the event that causes it is called the triggering event, or simply the trigger.

1.2

PAT: Process Analysis Toolkit

PAT is a self-contained framework for composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. 1.2.1 PAT Architecture

In PAT, each language is encapsulated as one module with predefined APIs, which identify the language syntax, well-formness rules as well as formal semantics, and loaded at run time according to the input model. This architecture allows new languages to be developed easily by providing the syntax rules and semantics. Three modules have been developed currently, namely Communicating Sequential Processes ( CSP ) module, RealTime System ( RTS ) Module and Web Service ( WS ) module. An extensible library of assertions, together with their verification algorithms, have been designed to operate on the underlying shared semantic models of the modules and therefore easily applicable to all modules. For instance, the automata-based LTL model checking algorithm, with partial order reduction, is applied to all modules. PAT architecture is shown in Fig. 2. 1.2.2 PAT System Components

The following are the four main components of PAT. Editor: User friendly editing envinronment (with advanced syntax editing features) for introducing models. Parser: Smart parsing to apply process equivalence laws to simply system models as well as associating assertions with the dedicated checker. Simulator: User friendly simulator for interactively and visually simulating system behaviors; by either random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc. Model Checkers: Click button model checker for deadlock-freeness verification, reachability analysis, state/event linear temporal logic verification (with or with fairness) and refinement checking

1.3

CSP: Communicating Sequential Processes

CSP is a formal language for describing patterns of interaction in concurrent systems. CSP was first described in a 1978 paper by C. A. R. Hoare, but has since evolved substantially. CSP has been practically applied in industry as a tool for specifying and verifying the concurrent aspects of a variety of different systems. As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely through message-passing communication. The relationships between different processes, and the way each process communicates with its 3

Figure 2: PAT Architecture.

Figure 3: PAT System Components.

4

environment, are described using various process algebraic operators. Grammar: P::= Stop | Skip | e→ P | P;Q | P Q | [ b ] P | P b Q | P Q | P \ X | P || P2 || P3||...||Pn | P1|||P2|||P3|||...|||Pn| P Q. The CSP process e→ P initially allows event a to occur and then behave subsequently as P. The process Q is executed after P in case of P;Q. The choice P Q offers an external choice between processes P1 and P2 whereby the choice is made by the environment. Conversely, P Q offers an internal choice between the two processes. The parallel combination P1 || P2 executes P1 and P2 in parallel. The process P1 ||| P2 executes P1 and P2 as interleaving process. In the process [ b ] P, b acts as guard conditon to execute P. In, P b Q, P is executed if boolean expression is true else Q is executed.

2

Previous Work

Many approaches of applying the model checking technique to UML state machines have been proposed before. Generally, these approaches translate UML specification into an intermediate model of some well-known model checker, such as SMV, SPIN and FDR. In the following we categorize them based on the model checkers used, and compare our work to the most relevant works in this area. The first work based on SPIN model checker is presented in 1991, by D. Latella, I. Majzik, and M. Massink. It presents a translation scheme for UML state diagrams into a Promela model and then invokes SPIN for verification. This work is constrained within the basic elements in state diagrams. Advanced modeling technique such as fork, join, history states, entry and exit behavior of states, variables and multiple state machines are not considered. In 1999, J. Lilius and I. P. Paltor present a tool called vUML which transforms a UML state machine to a Promela model. The technical details are not explained in that paper. Clarke and Heinle propose an approach to translating statecharts to the input language of symbolic model checker SMV in the year 2000. They map every state or event to a single variable. Inter-level transitions are excluded in their works. J. Dubrovin and T. Junttila define a semantics and a symbolic encoding of UML state machines, and performs verification on NuSMV model checker in 2007. They support deferring of messages, concurrent composite states and choice pseudo states. Later some works were proposed based on CSP which were similar to this work.

3

Proposed Work

Firstly, our approach supports a larger subset of UML state machines than most other works, including join, fork, history pseudo states, entry and exit points, which are commonly excluded or not well handled by previous works. Secondly, shared variables are extensively used to represent every state and event occurrence in state-based intermediate model, which arises the infamous state space explosion problem and hence degrades the performance of model checking. This approach alleviates this problem in the way that system behavior is directly specified in terms of processes and events, yet states are not explicitly represented. Lastly, the approach enjoys considerable benefits from the model checker PAT. Its simulator allows users to perform various simulation mechanisms 5

on the input model: complete states generation, automatically random simulation, user interactive simulation, trace replay and so on. On the other hand, its verifier enables users to check deadlock, reachability, trace refinement relationship, linear temporal logic properties with various fairness assumptions and etc. f : UML → CSP is defined to illustrate the fundamental mapping rules as Figure 4 shows. In the following, these rules are used to translate advanced modeling behavior involving composite and submachine states.

Figure 4: Translation Rules.

3.0.1

Fork

Fork state deals with the transition from a single source state to several substates in different regions of a composite state. When a transition from a fork state is fired, control passes to all the target states. If one or more regions have no target, then the initial states of all the other regions are implicitly chosen as the targets. The translation rule for fork is more involved than the previous ones. Generally, it reuses the rule for transitions between states at the same level by lifting the fork transition to the composite state, with annotations to describe the actual target, so that the target states are always under the influence of the composite stateâĂŹs own entry behavior and outgoing transitions. In detail, an n parameterized process is used to represent the composite state with fork transitions, in which n is the number of regions and every parameter denotes which state in a region is about to be activated. Therefore, a fork state specifies the targets by evaluating parameters, and every parameter is set to zero by default to represent initial state 6

for implicit entry. For example, the fork transition in Figure 5 is translated as follows:

Figure 5: Fork Pseudo State.

PS ( i, j, k ) = enter→ ( P1( i ) ||| ( P2 ( j ) ||| ( P3 ( k ) ); PF ork = PS(2, 0, 1); ... Pr2(i) = {case(i == 1) : Ps3; (i == 2) : Ps4; default : Pinitial2 }; 3.0.2 Join

Join state conversely specifies the transition from substates in different regions of a composite state to a target state outside the composite state. A join transition is effective only if all the source states are active. If triggered, it results in all the active substates of the composite state executing their exit behavior starting with the innermost states. Interlevel transition is a special case of a fork/join transition with single target/source. Regarding the translation, a common event is added to force the exit behavior execution of all source states in synchronization, such as the event join for the example in Figure 6. PS (i, j, k) = enterS0→ ( P1( i ) || ( P2 (j) || ( P3 (k) ); PS2 =(e2→exitS2→Skip) (join→exitS2→exitS0→ Pjoin ); PS4 =join→exitS0→ Pjoin ; PS5 =(e5→exitS5→Skip) (join→exitS5→exitS0→ Pjoin ); Pjoin =e6→PS6 7

Figure 6: Join Pseudo State.

4
4.1

Case Study
Farmer-Wolf-Goat-Cabbage Puzzle

State diagrams are often used to model puzzles or games. For example, one famous puzzle involves a farmer taking a wolf, a goat, and a cabbage to market. To do this, he must cross from the east to the west side of a river using a boat that can only carry him plus one of his three possessions. He cannot leave the wolf and goat together unsupervised, nor the goat and the cabbage, because one will eat the other. We can represent each state of this system by listing the objects that are on the east bank: w is the wolf, g is the goat, c is the cabbage, and f is the farmer. States like wc and wgb are legal, but wg would not be a legal state. The diagram of possible states looks as in Figure 7. And Figure 8 shows the simulaton for the puzzle in PAT Farmer-Wolf-Goat-Cabbage Puzzle in CSP: var farmer=0; var wolf=0; var goat=0; var cabbage=0; Cross()=[farmer==0 && (((wolf==0 && goat==0)) &&((goat==0 && cabbage==0)))] farmer_cross { farmer=1; } → Return() [farmer==0 && wolf==0 && ((goat==0 && cabbage ==0))] farmer_wolf_cross {

8

Figure 7: Farmer-Wolf-Goat-Cabbage Puzzle.

farmer=1;wolf=1; } →Return() [ farmer==0 && goat==0 ] farmer_goat_cross{farmer=1;goat=1;} → Return() [farmer==0 && cabbage==0 &&((wolf==0 && goat==0))] farmer_cabbage_cross { farmer=1; cabbage=1;} →Return(); Return()= [farmer==1 && (((wolf==1 && goat==1)) &&((goat==1 && carbage==1)))] farmer_return { farmer=1; } → Cross()

[farmer==1 && wolf==1 && ((goat==1 && carbage ==1))] farmer_wolf_return{farmer=0;wolf= Cross() [farmer==1 && goat==1] farmer_goat_return{farmer=0;goat=0;} → Cross() [farmer==1 && carbage==1 &&((wolf==1 && goat==1))] farmer_carbage_return{farmer=0;carba Cross() The Properties: #define goal (farmer==1&&wolf==1&&goat==1&&carbage==1); # assert Cross() reaches goal;

9

Figure 8: Simulation Window.

4.2

CD Player

Figure 9 shows a UML state machine diagram modeling a CD player. Initially, the player stays at composite state NONPLAYING. Thus, the whole process starts at NONPLAYING. CDPLAYER() = NONPLAYING(0); The composite state NONPLAYING starts at CLOSED state, which denotes the CD drawer is closed. When a user presses load button, the drawer opens. If he/she presses it again, the drawer closes and the track ready to be played and track is set to the first one in CD. When the user presses play button, if no CD is in the drawer, then the drawer keeps closed; otherwise, the player goes to BUSY state. Using the translation rules to map NONPLAYING state to a CSP process we obtain the following CSP program. //Variable declaration var present = false, track = 0; //Process definition NONPLAYING(i) =case{ (i == 0) : CLOSED() (i == 1) : OPEN() } (([present](play → NONPLAYING(0))) ([present](play → BUSY(0))) (off → Skip));

10

CLOSED() = load → open {track = 0; present = false} → OPEN(); OPEN() = load → close{track = 1; present = true} → CLOSED(); When it enters BUSY state, the player firstly locates the track to play and starts to play one by one until the last track is finished and after that the player goes back to CLOSED state. If play button is pressed with the player in BUSY state, the player enters the history state. In other words, it plays the current track if PLAYING is the last active substate; it restarts the current track but remains paused if PAUSED is the last one. Since history state is used, a shared variable j is defined to retain the last visited substate. Its valuation behaves as the entry behavior of every substate. Thus, BUSY state is described as the following.

Figure 9: CD Player States.

//N denotes the total number of tracks. var j = 0; BUSY(i) = find track start → case{(i == 0) : PLAYING() (i == 1) : PAUSED()} ((load → NONPLAYING(1)) ( ] track = N ] ( {track = track + 1} → BUSY(0))) ( [track == N]NONPLAYING(0)) (stop → NONPLAYING(0)) (off → Skip) 11

(play → BUSY(j)); PLAYING() = {j = 0; } → (play track → Skip) ((pause → PAUSED()) Skip); PAUSED() = {j = 1; } → pause → PLAYING(); The results from PAT suggest that the design satisfies the safety properties stated above. Also, other kinds of property assertions could be verified against the model with the help of PAT, such as liveness, fairness and trace refinement properties. Take a liveness property as an example: a CD player should ensure that when there is a CD in the drawer, if the user presses play button, then the player will eventually play some track. When we model-check the property against the model, it turns out that the model satisfies it.

5

Conclusion

In this the definition a translation scheme for a class of UML models composed of asynchronously executing, hierarchical state machines has been defined. The main purpose of this approach is two-fold: first, to provide a completely automatic approach for transforming a model of state machines to the input model of PAT model checker; second, to effectively handle advanced modeling techniques in state machines such as fork, join, history and submachine features.

12