uppaaltutorial (Uppaal - описание)

Chapter 1A First Introduction to UppaalFrits VaandragerAbstract This chapter provides a first introduction to the use of the model checkingtool Uppaal. Uppaal is an integrated tool environment that allows users to model thebehavior of systems in terms of states and transitions between states, and to simulateand analyze the resulting models. Uppaal can also handle real-time issues, that is,the timing of transitions. Using an example of a jobshop, we explain in a step bystep manner how one can make a simple Uppaal model, simulate its behavior andanalyze properties.1.1 Introduction1.1.1 Model CheckingModel checking [5, 3, 1] is a powerful technique for automated debugging of complex reactive systems such as hardware components, embedded controllers and network protocols. In model checking, specifications about a system are expressed as(temporal) logic formulas, and efficient symbolic algorithms are used to traverse themodel defined by the system and check if the specification holds or not.

In 2007,E.M. Clarke, E.A. Emerson and J. Sifakis were awarded the ACM Turing Award fortheir roles in developing model checking into a highly effective verification technology, widely adopted in industry.Model checkers allow one to analyze models that capture the dynamic behaviorof systems. These can be all sorts of systems: a network of computers or a printer, aSudoku puzzle or an ant colony, an autonomous robot or train control software, etc.Actually, in principle any system can be analyzed using a model checker, as longFrits VaandragerInstitute for Computing and Information Sciences, Radboud University Nijmegen, Heijendaalseweg 135, 6525 AJ Nijmegen, The Netherlands, e-mail: F.Vaandrager@cs.ru.nl.2Frits Vaandrageras it has states and transitions between states.

In order to illustrate the concept ofmodel checkers, we consider the following puzzle:Six girls each know a secret. By means of a series of bilateral conversations(regular phone conversations, say) they want to exchange all secrets. Whenever two girls have a conversation they share all the secrets they know at thetime. How many conversations are needed before every girl knows every secret?Figure 1.1 shows a state-transition diagram or automaton for the simplified version of the problem in which there are 3 girls. A state consists of a 3 by 3 matrixknows that records for each girl the gossips she knows. If girl i knows the gossipof girl j then we write a 1 in the entry for row i and column j: knows[i][j] == 1.Otherwise we write a 0: knows[i][j] == 0.

In the initial state, at the top of the diagram, each girl only knows her own gossip, and hence there are 1’s on the diagonaland 0’s elsewhere. Transitions between states occur whenever girls have a conversation. In the initial state three transitions are possible: girls 1 and 2 call each other,1 0 00 1 00 0 11 1 01 1 00 0 11 1 11 1 01 1 11 1 01 1 11 1 11 0 10 1 01 0 11 1 11 1 11 0 11 0 11 1 11 1 11 0 00 1 10 1 11 1 11 1 10 1 11 1 10 1 11 1 11 1 11 1 11 1 1Fig.

1.1 State space for 3 gossiping girls.girls 1 and 3 call each other, and girls 2 and 3 call each other. In the new states, therows for the corresponding girls are adjusted and all gossips are exchanged. Not allconversations lead to a new state: sometimes a conversation does not produce any1 A First Introduction to Uppaal3new information for any of the participants, and there is just a loop from the state toitself. Altogether 11 states can be reached starting from the initial state, and at least3 conversations are needed before every girl knows every gossip.Properties of state-transition diagrams can be described in the language of temporal logic. For instance, if ϕ is a property of states, then the temporal logic formula E ϕ describes the property “there exists a path that leads to a state in whichϕ holds”.

Model checkers can compute whether a temporal logic formula holdsfor (the initial state of) a given state-transition diagram. We can solve the gossiping girls puzzle by asking a model checker to produce the shortest diagnostic tracethat shows that the formula E “each girl knows each gossip” holds for the statetransition model for 6 girls.

In the syntax of the model checker Uppaal:E<> forall (a : girls) forall (b : girls)knows[a][b] == 1Figure 1.2 shows the solution for the gossiping girls puzzle that was found by Uppaal: at least 8 conversations are needed before every girl knows every secret. In fact,the message sequence diagram displayed in Figure 1.2 has been directly generatedby the Uppaal tool.Although utterly simple, the gossiping girls example already illustrates severalkey features of model checkers:1. No proofs. Mathematicians have established that, in general, n girls need at least2n − 4 conversations to exchange all gossips [8].

The result of [8] required ingenuity and hard work, whereas Uppaal produces its solution for the special casen = 6 fully automatically.2. Fast. Using his of her favourite model checker, an experienced user can constructa model for the gossip puzzle within half an hour. Uppaal needs a few minutes tofinding the optimal solution for n = 6, and just a few seconds to find an optimalsolution for the cases n < 6.3. Diagnostic counterexamples. Model checkers are very good at finding unexpected scenarios.

When trying to solve the gossip puzzle, most people quicklycome up with a solution that requires 9 conversations. The optimal solution foundby Uppaal, which only requires 8 conversations, is tricky and much harder to findfor humans. In industrial applications, model checkers often produce unexpectedevent orders that lead to an error state, fast solutions for scheduling problems, etc.The diagnostic counterexamples produced by model checkers frequently providekey insights in a design.4. State space explosion.

Since states of the model for n girls are n × n Boolean2matrices, the number of states of the model will be in the order of 2n and hencegrows exponentially in n. Using some special verification features (symmetry reduction and the sweepline method), Uppaal can handle up to 7 girls (see Chapter2 Add ref). Despite these limitations, in practice we often see that analysis ofsmall instances of a parametrized model already produces important insights. Itis trivial to generalize the solution with 8 conversations for n = 6 of Figure 1.2to a general solution with 2n − 4 conversations for n > 6.

Similarly, if a design4Frits Vaandragercontains a flaw then usually this flaw can already be revealed by model checkinga small instance of the design.1.1.2 UppaalThis chapter provides a first introduction to the use of the model checking toolUppaal. Uppaal is an integrated tool environment that allows users to model thebehavior of systems in terms of states and transitions between states, and to simulateand analyze the resulting models. Uppaal can also handle real-time issues, that is,the timing of transitions.

Using an example of a jobshop, we will explain in a stepby step manner how one can make a simple Uppaal model, simulate its behavior andanalyze properties.Uppaal is available for free for non-commercial applications in academia and forprivate persons via www.uppaal.org. For commercial applications a commerciallicense is required, see www.uppaal.com. The software runs under Windows,Fig. 1.2 Solution for gossiping girls puzzle found by model checker Uppaal.1 A First Introduction to Uppaal5Linux and Mac OS X. Installation is usually trivial.

The only requirement is that Javaversion 6 (e.g. J2SE Java Runtime Environment) or newer has been installed andproperly configured on the system. Uppaal is developed in collaboration betweenthe Department of Information Technology at Uppsala University in Sweden andthe Department of Computer Science at Aalborg University in Denmark, with inputfrom several other universities around the world (including the author’s group fromthe Radboud University Nijmegen).Uppaal is a toolkit with a wealth of possibilities to model and analyze systems.

Inthis chapter, we will restrict attention to the absolute basics. The next chapter of thishandbook will give an overview of some of the more advanced features of Uppaal.More details and documentation can also be found on the Uppaal website and inthe tutorial paper [2] (the last article requires some background in formal methods).The help menu within Uppaal also provides an excellent explanation of the variousfeatures and possibilities of the tool. Actually, some text in this chapter has beendirectly taken from the help menu.There are numerous other model checkers that one can freely download from theinternet: Spin, Blast, MCRL2, Java Pathfinder, etc.

We refer to [11] for an overview.Advantages of Uppaal are the graphical user interface and the short learning curve.After you have spent half a day on reading this tutorial and following the detailledinstructions for building and analyzing some simple models, you can already startusing the tool yourself.1.2 A jobshopWe will now explain step by step how a simple production line can be modeled inUppaal.

This example is due to Robin Milner; we have taken the following description and illustration of Figure 1.3 from [10]:We suppose that two people are sharing the use of two tools — a hammer anda mallet — to manufacture objects from simple components. Each object ismade by driving a peg into a block. We call a pair consisting of a peg anda block a job; the jobs arrive sequentially on a conveyor belt, and completedobjects depart on a conveyor belt. The jobshop could involve any numberof people, whom we shall call jobbers, sharing more or fewer tools.

In thischapter, we assume a system with two jobbers and a hammer and a mallet. Tomake the example more specific, we shall assume that the nature of the jobinfluences the jobber’s actions in a particular way. We suppose that he mayuse two predicates easy and hard over jobs, to determine whether a job is easyor hard or neither. He will do easy jobs with his hands, hard jobs with thehammer, and other jobs with either hammer or mallet.6Frits VaandragerFig. 1.3 A jobshop (picture taken from [10]).1.3 The system editorAfter starting Uppaal, we see the window displayed in Figure 1.4. The Uppaalgraphical user interface consists of three main parts, accessible via three tabs in themain window: the system editor, which can be used to construct models, the simulator, in which the behavior of models can be simulated, and the verifier, in whichthe behavior of models can be analyzed.