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

In this schedule, the final transitions from thejobbers back to the begin state are missing, but these transitions take no time. Soeven when the jobbers always start working on jobs as soon as they can, and immediately grab tools whenever they become available, the worst case schedule is still26 time units slower than the fastest schedule from Figure 1.15. Figure 1.17 visualizes the slowest schedule as a Gannt chart. At time 0, Jobber1 grabs the firstFig. 1.17 Slowest schedule for completing the 10 jobs.(hard) job, and Jobber2 grabs the second (average) job.

Of course, in any reasonable scenario, Jobber1 would use the hammer and Jobber2 the mallet. But26Frits Vaandragerin the worst case scenario of Figure 1.17, Jobber2 gets the hammer, and henceJobber1 has to wait. Until time 78 one jobber is using the hammer while theother jobber is idling.

At the end of the schedule, after Jobber2 has finished job9, Jobber2 is still working for some time on job 10 using the mallet.1.9 Parameters and arraysIn this section, we will discuss two useful features of Uppaal, that allow us to describe our jobshop model more compactly: template parameters and arrays.1.9.1 ParametersIn the jobshop model, we have defined a single template Jobber with two instancesJobber1 and Jobber2.

Likewise, we would like to have a single template Toolwith two instances Hammer and Mallet. It is possible to define this in Uppaalusing the notion of Parameters. Parameters can be declared to have either call-byvalue or call-by-reference semantics, that is, a template may have access to eithera local copy of the argument or to the original. The syntax is taken from C++,where the identifier of a call-by-reference parameter is prefixed with an ampersendin the parameter declaration.

Clocks and channels must always be call-by-referenceparameters.freeget?takenput?Fig. 1.18 Generic model of template Tool.Figure 1.18 shows the definition of the generic template Tool. In the field Parameters at the top of the Editor tab, we declare the two channel names that are usedas parameters in this template:urgent chan &get, chan &putIn the System declarations section, we can now define Hammer and Mallet asinstances of Tool:Hammer = Tool(get_hammer,put_hammer);Mallet = Tool(get_mallet,put_mallet);1 A First Introduction to Uppaal27The old templates Mallet and Hammer can be deleted via the Remove templateoption in the Edit menu.

Our new model has exactly the same behavior (in terms ofglobal states and transitions) as the old model, but due to the use of parameters thedefinition has become shorter.1.9.2 ArraysThe model of the belt of Figure 1.13 is not easy to extend or reuse: each time wewant to study a new arrival pattern of jobs, we have to redraw the automaton. Thisis cumbersome, especially if we want to schedule a batch with a large number (sayhundreds) of jobs.

It is also more natural to define the arrival pattern as a datastructure rather than as a control structure (automaton). We can describe the jobarrival pattern as a (constant) integer array as follows:const int E=0;const int A=1;const int H=2;const int J=10;const int[0,2] jobs[J] = {H,A,H,H,H,E,E,A,A,A};Uppaal does not support enumerated types and therefore we use 0 to encode easyjobs (E), 1 to encode average jobs (A), and 2 to encode hard jobs (H). As before, theinteger constant J denotes the total number of jobs in the batch.

The one dimensionalconstant array jobs specifies the arrival pattern of jobs (which is identical to thepattern in Figure 1.13). The size of the array equals J (counting from 0 to J −1) and the range is the set {0, 1, 2} or equivalently {E, A, H}. Figure 1.19 shows ageneric model for the Belt template that uses the information from the array jobsto generate the appropriate sequence of jobE!, jobA! and jobH! transitions.

Theautomaton uses an auxiliary variableint[0,J] i;that records the number of jobs that has been delivered thus far. Again, the newmodel has exactly the same behavior (in terms of global states and transitions) asthe old model, but due to the use of arrays the definition has become shorter andeasier to reuse.1.10 What is a good model?After having presented the basic functionality of the Uppaal tool, we want to conclude this chapter with some general recommendations for constructing models.

Tosome extent, building good models is an art. Dijkstra’s motto “Beauty is our business” [4] applies to models as well as to programs. Nevertheless, we can state seven28Frits Vaandrageri<J && jobs[i]==HjobH!i++i<J && jobs[i]==EjobE!i++i<J && jobs[i]==AjobA!i++Fig. 1.19 Generic model of template Belt.criteria for good models.5 These criteria are in some sense obvious, and any personwith experience in modelling will often try to adhere to them. Often some criteriaare hard to meet and typically several of them are conflicting. In practice, a goodmodel is often one which constitutes the best possible compromise, given the current state-of-the-art of tools for modelling and analysis.1.

A good model has a clearly specified object of modelling, that is, it is clear whatthing the model describes. The object of modelling can be (a part of) an existingartefact or physical system, but the object may also be a document that informallyspecifies a system or class of systems (for instance a protocol standard), and itmay even be a collection of ideas of a design team about a system they construct,expressed orally and/or by some drawings on a whiteboard.In the case of our jobshop example, the object of modelling is the informal specification that is contained in the grey boxes throughout this chapter.2. A good model has a clearly specified purpose and (ideally) contributes to therealization of that purpose. Possible purposes include: communication betweenstakeholders about a design, a specification of a system, verification of specific properties (safety, liveness, timing,..), analysis and design space exploration,code generation, and test generation.

A model can be descriptive or prescriptive.If a model has to serve several distinct purposes then often it is better to constructmultiple models rather than one.The only purpose of the jobshop models constructed in Sections 1.3 up to 1.7is to explain the use of the Uppaal tool. The models in Section 1.8 serve theadditional purpose that they help us to answer the timing related questions statedin the grey boxes.3.

A good model is traceable: each structural element of a model either (1) corresponds to an aspect of the object of modelling, or (2) encodes some implicitdomain knowledge, or (3) encodes some explicit additional assumption. Additional assumptions are for instance required when a protocol standard is incomplete (e.g., it does not specify how to handle certain events in certain cases).Links between the structural elements of the model and the aspects of the object of modelling should be clearly documented. A distinction must always be5Most of these criteria are described by Mader, Wupper and Boon [9]. We refer to [9] for furtherlinks to related work in the areas of software engineering, requirements analysis, and design.1 A First Introduction to Uppaal29made between properties of (a component of) a model and assumptions aboutthe behavior of its environment.Our jobshop models are traceable: in the text we explain for each element in amodel how it relates to the informal specification.4.

A good model is truthful (or valid): relevant properties of the model should alsocarry over to (hold for) the object of modelling. Typically, for each (relevant)behavior of the object of modelling there should be a corresponding behavior ofthe model. In the construction of models often idealizations or simplificationsare necessary in order to allow for the use of a certain modeling formalism orin order to be able to analyze the model.

In these cases, the model may not beentirely truthful. The modeller should always be explicit about such idealizations/simplifications, and have an argument why the properties of the idealizedmodel still say something about the artefact. In the case of quantitative modelsthis argument will typically involve some error margin. In the case of timed automata models it frequently occurs that a model “overapproximates” reality andthat, due to nondeterminism, certain behaviors that are possible in the model arenot possible for the artefact.The untimed model of Section 1.7 is certainly truthful to the informal specification of Milner listed in the grey box in Section 1.2.

However, in the timed modelof Section 1.8 there is at least one idealization that is not entirely realistic. Ourmodel assumes that it takes no time to grab a job from the conveyor belt. Or moreprecisely: that no time elapses between starting to pick a job from the belt andstarting to pick a tool. Since a job consists of both a peg and a block, it is reasonable to assume that a jobber needs both hands to grab a job from the conveyorbelt. Hence it is not possible to grab a job and a tool simultaneously, and if wereally want our model to be thruthful, we should add extra transitions that correspond to the end of the activity to grab a job, and we should give lower and upperbounds for the duration of this activity. In the jobshop example the criterion ofthruthfulness collides with our next criterion of simplicity: in order to keep ourmodel simple we compromised a bit on thruthfulness.5. A good model is simple (but not too simple).

Occam’s razor is a principle particularly relevant to modelling: among models with roughly equal predictive power,the simplest one is the most desirable. Hence, the number of states and state variables should be as small as possible, and the level of atomicity of transitionsshould be as coarse grained as possible (but not coarser), i.e., the number of transitions should be minimal given the intended use of the model. Preferably, thingsshould be written only once, and one should avoid ugly encodings.

Preferably,the model uses stable, well-defined and well-understood concepts and semantics.The model of Section 1.9 is almost maximally simple. We would have likedto simplify the automaton of Figure 1.19 even further so that it only has onetransition instead of three. But this is not possible since Uppaal does not allowdata parameters for synchronization channels.6. A good model is extensible and reusable, that is, it has been designed to evolveand be used beyond its original purpose. Typically, if one defines models ina modular and parametric way this allows for dimensioning, future extensions30Frits Vaandragerand modifications, especially if modules have well-defined interfaces.