uppaaltutorial (Uppaal - описание), страница 3

The otherautomaton has do something else or has to wait until the next a! synchronizationwill be offered. In our jobshop example it does not matter which transition is labeledwith a! and which transition is labeled with a?. Often, we place the a! on a transitionof the component that takes the “initiative” for the synchronization. In the case of thejobshop, the jobbers take the initiative to grab a tool, whereas the tools are passiveand just “wait” until someone is using them. Hence, we place the !’s in the templatefor the jobbers, and the ?’s in the templates for the tools.

Figure 1.9 shows theadjusted model of the jobber, in which synchronization channels have been added.Synchronization channels must also be declared. This can be done by clicking on the(global) project Declarations in the window on the left, and inserting the followingtext:// Place global declarations here.chan get_hammer, put_hammer, get_mallet, put_mallet;If we simulate the extended model, we quickly see that in the new model “deadlocks” are possible, states from which no transition is enabled.

This occurs, forinstance, when both jobbers are in location hard and both want to perform aget hammer! transition. But since there is no automaton that can perform amatching get hammer?, the system comes to a crunching halt. In order to ruleout these deadlocks, we add new templates Hammer and Mallet (this can be doneby selecting the option Insert Template in the Edit menu). Figure 1.10 shows the def-12Frits Vaandragereasywork_easywork_av_malletput_mallet!get_mallet!averagebeginwork_av_hammerget_hammer!put_hammer!work_hardget_hammer!put_hammer!hardFig. 1.9 Model of jobber, extended with synchronization labels.initions of these templates.1 We add the new automata to the System declarationsvia the textsystem Jobber1, Jobber2, Hammer, Mallet;We have now completed our first Uppaal model! We can open the model in thesimulator and convince ourselves that it indeed behaves as specified in the informaldescription.

Once we are satisfied with the model, we can save it by selecting in theFile menu the option Save System As.... Uppaal models are stored as .xml files.freeget_hammer?takenput_hammer?freeget_mallet?takenput_mallet?Fig. 1.10 Models of hammer and mallet.1Actually, it would be better to have just one template Tool, with two instances Hammer andMallet. It is possible to define this in Uppaal, but this involves adding channel names as parameters to a template. Since we prefer to explain the notion of template parameters in Section 1.9 ofthis chapter, we introduce separate templates for hammer and mallet.1 A First Introduction to Uppaal131.6 The verifierThe Simulator is extremely useful for playing with a model and obtaining insight,but it does not answer questions like “Is it possible to reach a state in which (somegiven) property Bad holds”? Even if we have not seen a Bad state after hours ofsimulation, this does not guarantee that no such state exists! Fortunately, Uppaal’sVerifier allows us to rigorously answer this type of questions.Fig.

1.11 Screenshot of the Verifier.1.6.1 QueriesWithin the Verifier, we can specify a so-called Query, a property that may or maynot hold for a given model. By exhaustive exploration of the set of reachable states(the “state space”), the Verifier can establish whether a Query is satisfied or not.Figure 1.11 shows a screenshot of the Verifier. Queries often start with the symbols“A[]”. This notation, which is taken from the field of temporal logic, means “In allreachable states it is the case that”. Thus, for example, the query14Frits VaandragerA[] not deadlockstates that in all reachable states of the system there is no “deadlock”.

Recall that astate has a “deadlock” if it has no outgoing transitions. Stated differently, the abovequery asserts that in all reachable states at least one transition is possible. If wetype the query in the Query window of the Verifier and then press the Check button,Uppaal explores all the reachable states to see if they have an outgoing transition.

Inthe case of our model this is indeed the case, and therefore Uppaal returns Propertyis satisfied. This means that in each of the reachable states always either Jobber1or Jobber2 can proceed.A new query can be entered by pressing the Insert button, and typing the queryin the window Query. We may for instance enter the following text:E<> (Jobber1.work_hard && Jobber2.work_hard)Here the notation “E<>”, again taken from temporal logic, means “There exists areachable state such that”.

The above query asserts that there exists a reachable statein which that Jobber1 and Jobber2 are in location work hard, that is, bothjobbers are working on a hard job. Much of the syntax of Uppaal is similar to thatof common programming languages such as C, C++, Perl and Java. For instance,&& denotes logical “and”: it combines two boolean values and returns true if andonly if both of its operands are true. When we ask Uppaal to check the above query,the result is Property not satisfied. This is what we expect: if a jobber is workingon a hard job he is using the hammer, and since there is only one hammer, at mostone jobber can work on a hard job at a time.

Note that Uppaal does not use anyclever form of reasoning to arrive at this conclusion. The tool just uses brute forceto explore all the reachable global states of the model and to check for each of thesestates whether both jobbers are working on a hard job.In the Uppaal help menu the full syntax for queries and expressions is described.In this chapter, we only consider queries of the form A[]e and E<>e, where e isan expression. An expression e consists of a boolean combination of atomic propositions. Atomic propositions can be of the form A.l, for A an automaton and l alocation.

Such a proposition is true in a global state of the model if in this state automaton A is in location l. Table 1.1 gives some examples of boolean operators thatcan be used in Uppaal. Further on in this chapter we will encounter other types ofproperties.Symbol&&||==implynotOperator nameandorequalityimplicationnegationMeaninge && f is true if both e and f evaluate to truee || f is true if e evaluates to true or f evaluates to truee == f is true if e and f evaluate to same valuee imply f is true if e evaluates to false or f evaluates to truenot e is true if e evaluates to falseTable 1.1 Some logical operators in Uppaal1 A First Introduction to Uppaal151.6.2 Diagnostic tracesWe can ask Uppaal whether there exists a reachable state in which one jobber isworking on an average job with a mallet, and the other jobber is working on aaverage job with the hammer:E<> (Jobber1.work_av_mallet && Jobber2.work_av_hammer)Uppaal then answers Property is satisfied. In this case, Uppaal can also provide aconcrete example that illustrates why the property holds, that is, a trace leading toa state in which the first jobber is working on an average job using the mallet, andthe second jobber is working on an average job using the hammer.

In order to letUppaal compute such an example, we choose under Options the entry DiagnosticTrace and then select the option Shortest. If we now let Uppaal check the aboveproperty again, it will again produce the answer Property is satisfied but in addition it will compute the shortest path (or trace) leading to a state in which bothJobber1.work av mallet and Jobber2.work av hammer hold. The toolasks whether it may store this path in the simulator.

If we give Uppaal permission todo this, we can replay the trace in the simulator. If we open the simulator, then wesee the final state of the trace in which Jobber1 is in location work av malletand Jobber2 is in location work av hammer. By pressing the Reset button wego to the initial state of the trace, and by pressing the Replay button we tell Uppaalto replay the trace within the simulator. We can also replay the trace step-by-step byrepeatedly pressing the lowest Next button.In general, Uppaal can provide a diagnostic trace for E<> properties that hold,and for A[] properties that do not hold. In the case of E<> properties that donot hold, or A[] properties that hold, Uppaal can only report that it exhaustivelychecked all the reachable states of the model and didn’t find anything. In the aboveexample of an E<> property, the diagnostic trace is rather trivial and consists ofonly four transitions. However, in realistic models of industrial applications, diagnostic traces may describe tricky scenarios involving thousands of transitions.

Insuch cases, Uppaal’s ability to provide diagnostic traces is extremely useful. Forinstance, if Uppaal tells us that a certain correctness property does not hold, an engineer typically wants to know why this is the case.1.6.3 Saving queries and tracesWe can save queries by selecting in the File menu the option Save Queries As....The queries are then saved as a text file with extension .q.

If one opens a Uppaalmodel model.xml, then automatically also the query file model.q is opened (ifit exists). Alternatively, one can open a query file by selecting in the File menu theoption Open Queries.... It is also possible to save traces by pressing the Save buttonin the simulator. Traces are saved as (unreadable) text files with extension .xtr. Atrace file can be opened by pressing the Open button in the simulator.16Frits Vaandrager1.6.4 How many states are there?Let us try to compute the total number of reachable states of our jobshop model.Since each jobber is modeled by an automaton with 8 locations, and each tool ismodeled by an automaton with 2 locations, there are at most 8 × 8 × 2 × 2 = 256global states.

However, many of these states can not be reached from the initial state:they will never occur in any run of the system. In order to see this, observe that oncewe know the state of the two jobbers, we also know the state of the two tools:A[] Mallet.taken == (Jobber1.work_av_mallet|| Jobber2.work_av_mallet)A[] Hammer.taken == (Jobber1.work_av_hammer|| Jobber1.work_hard|| Jobber2.work_av_hammer|| Jobber2.work_hard)The first query states that the mallet is taken exactly when either the first or thesecond jobber uses it for an average job. The second query states that the hammeris taken exactly when either the first or the second jobber is using it for either anaverage or a hard job.

Since the locations of both mallet and hammer are fully determined by the locations of the jobbers, this means that our model has at most8 × 8 = 64 global states that are reachable from the initial state.Five of these remaining 64 states can not be reached since the mallet and hammercan only be used by one jobber at a time:A[]not&¬&¬&¬&¬(Jobber1.work_av_mallet && Jobber2.work_av_mallet)(Jobber1.work_av_hammer && Jobber2.work_av_hammer)(Jobber1.work_av_hammer && Jobber2.work_hard)(Jobber1.work_hard&& Jobber2.work_av_hammer)(Jobber1.work_hard&& Jobber2.work_hard)All the other combinations of locations of Jobber1 and Jobber2 can be reached,and so the total number of reachable states of our model is 64 − 5 = 59.2 For Uppaalour model is really small: the program can easily handle models with thousands oreven millions of states. It is trivial to construct models that are so big that Uppaalcannot handle them and, for instance, runs out of memory.