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

In this subsection we discuss the systemeditor, subsection 1.4 will present the simulator, and subsection 1.6 will present theverifier. Upon starting Uppaal, at first the system editor is displayed.A Uppaal model (called system) is defined as a composition of a number of basic components (called automata or processes). Automata are diagrams with states(called locations) and transitions between states (called edges).The system editor has four drawing tools for building automata, see Figure 1.5,named Select, Location, Edge and Nail.• The Select tool is used to select, move, modify and delete elements. Elementscan be selected by clicking on them or by dragging a rubber band around one ormore elements. Elements can be added or removed from a selection by holdingdown the control key while clicking on the element.

The current selection can bemoved by dragging them with the mouse. Double clicking an element brings upa menu in which properties for that element can be specified. Right clicking anelement brings up a pop-up menu from which properties of the element can bechanged.• The Location tool is used to add new locations. Simply click with the left mousebutton in order to add a new location. Be careful: if one clicks several times newlocations will be stacked on top of each other (a common mistake, leading to1 A First Introduction to Uppaal7Fig.

1.4 Uppaal after starting the toolkit.Fig. 1.5 The four drawing tools Select, Location, Edge and Nail.models with strange behavior). In order to move a location to another position orto edit its properties, one first has to return to the Select tool.• The Edge tool is used to add new edges between locations. Start the edge byclicking on the source location, then click in order to place nails and finally clickthe target location. The operation can be cancelled by pressing the middle orright mouse button. It is possible to change the source and target of an edge bymoving the mouse to the beginning or end of an edge until a small circle appears(the “nail”). Drag this circle to a new location in order to change the source ortarget of the edge.• The Nail tool is used to add new nails to an edge, that is, places where an edgemay change direction.

Simply click and drag anywhere on an edge to add andplace a new nail.We will now construct our first Uppaal model. In the field Name at the top ofthe drawing window we enter the name of the first component (“template”) of our8Frits Vaandragermodel: Jobber. Next we right click (with the Select tool) on the location whichUppaal has already placed in the drawing window. We can then give this location aname, for instance begin.

Each automaton has at most one initial location, markedby a double circle. During simulation or in verifications the automaton will alwaysstart in this location. By checking the box Initial in the menu for a location, wespecify that this location is the initial location of the automaton. The menu containsa couple of other fields and options (Invariant, Urgent and Committed), but for themoment we will not use these.Fig. 1.6 A first version of the model.We can continue drawing and construct the automaton that is depicted in Figure 1.6. The first transition from the initial location corresponds to the moment whena jobber picks a new job from the conveyor belt.

There are three transitions possible since according to the informal specification there are three types of jobs: easyjobs, hard jobs and jobs with average difficulty (neither easy nor hard). The nexttransition corresponds to the moment at which the jobber grabs a tool (if needed)and starts working on the job. In the case of a job with average complexity, there aretwo possible transitions, depending on the tool that is selected. The third transitioncorresponds to the moment that the jobs is done: the automaton returns to its initialstate and the jobber is ready for the next job.1 A First Introduction to Uppaal9At this point, we have not specified in our model how the choice between thetransitions from location begin to location easy, average or hard is made.Also, we have not specified how the choice between the transitions from location average to location work av mallet and work av hammer is made.Choices for which the model does not specify how they are resolved are callednondeterministic.

Nondeterminism is very useful for maintaining a high level ofabstraction in descriptions of the behavior of physical systems and machines [6].Fig. 1.7 Declaration of system components.Once we have constructed the automaton of Figure 1.6, our first model is almostready.

Click on System declarations in the left window. We now see a screen inwhich one can list all the processes (automata) in a model. As shown in Figure 1.7,we specify that our first model consists of two instances of the template Jobber,called Jobber1 and Jobber2. So our model consists of two automata that, intuitively, run in parallel. As we will see, a global state of the full model is fullydetermined by the locations (states) of its components, and the transitions of the fullmodel are in direct correspondence with the edges (transitions) of its components.By clicking on Tools in the menu bar at the top of the screen, and then on CheckSyntax, we may check whether a model is syntactically correct.

If a model containsmistakes, these will be underlined in red. A more detailed description of the errorsis provided in a window at the bottom of the screen (normally not visible, but onecan make it larger using the mouse).1.4 The simulatorOnce a model is syntactically correct, we can simulate it, that is, explore the statespace of the model in a step-by-step fashion, by selecting the tab Simulator. Theresulting screen is displayed in Figure 1.8.

Uppaal makes two copies of the template10Frits VaandragerFig. 1.8 Screenshot of the simulator.Jobber, one for each automaton instance. Using red dots the current location ofeach automaton is highlighted. Initially, the current location of an automaton is itsinitial location. In the simulation control panel on the left, we see that (due to nondeterminism) six transitions are possible from the initial state (three for each jobber).When we select one of these transitions, the corresponding step in the automatondiagram for Jobber1 or Jobber2 is colored red.

Pressing the Next button causesthe simulated system to take the selected transition, and to update the current location. Using the Prev button one can go to the previous step in a simulation trace,with the Reset button one can bring the system back to its initial state, and withthe Replay button one can instruct Uppaal to automatically replay the current trace.If we press the button Auto, then Uppaal starts executing randomly selected transitions, one after the other. The speed of the simulation can be changed by moving thearrow in between Slow and Fast. We can stop the random simulation by pressing theAuto button again.1 A First Introduction to Uppaal111.5 ChannelsThe simulator is very useful for obtaining insight in the behavior of a model andfinding mistakes. By playing with our first model in the simulator, we quickly discover that something is wrong: both jobbers can be in location work hard simultaneously.

This should not be possible, since in this location both jobbers are usingthe hammer, and there is only one hammer. Hence we need to refine/correct ourmodel.In order to fix the model, we introduce separate templates for both the hammerand the mallet. For each tool there are 2 locations: free or taken. The automatonfor a tool moves from location free to location taken when it is grabbed by oneof the jobbers.

In order to model the synchronization between tools and jobbers,we use the notion of (synchronization) channels from Uppaal. Once “a” has beendeclared as a channel, transitions can be labeled with either a! or a?. This can bedone by double clicking (within the Editor) transitions with the Select tool, and thenwriting a! or a? in the Sync field. When two automata synchronize on channel “a”,this means that an a! transition of one automaton occurs simultaneously with ana? transition of another automaton. An a! or a? transition can never occur on itsown: a! always has to synchronize with a?, and vice versa. If there is one automatonS that can do an a! but two automata R1 and R2 that can do an a?, then there isa nondeterministic choice and S can synchronize with either R1 or R2.