所需积分/C币:39 2017-11-29 16:11:42 752KB PDF
收藏 收藏

nienu inside the tool. We use the following notations: c is a set of clocks and B(C)is the set of conjunctions over simple conditions of the form .c D c or x-y凶c. where m,y∈C,c∈Nand∝∈{<,≤,=,≥,>}. a timed automaton is a finitc directed graph annotated with conditions ovcr and resets of non-ncgativc real valued clocks Definition 1(Timed Automaton (TA)). A timed automaton is a tuple (L, Lo, C, A, E,I, where L is a set of locations, lo E L is the initial location C is the set of clocks, A is a set of actions, co-actions and the internal T-action E∈L×A×B(C)×2C× l is u set c! edges betweent locations with un act a guard and a set of clocks to be reset, and I: L-B(C)assigns invariants to locations In the previous cxamplc on Fig. 1, y:=0 is thc resct of thc clock y, and the labels press? and press! denote action co-action(channel synchronisations here) We now define the semantics of a timed automaton . a clock valuation is a function u: C-R>o from the set of clocks to the non-negative reals. Let o be the set of all clock valuations. Let uo(r)=0 for all T E C. We will abuse the notatioN by considering guards and invariants as sets of clock valuations, writing I( to mean th cities 1( Fig. 2. Semantics of TA: different transitions from a given initial state Definition 2(Semantics of TA). Let (L, l o, C, A,E, I be a timed automaton The semantics is defined us a labelled trurisilion systen(S, 50, -),where S=Lx rc is the set of states,so=(n,o0) is the initial state,and→sS×(R>0UA)×S tion relati ch that ,u)→(l,a+d)iV:0≤≤d=t+d∈I().nd (L, u)(I, u)if there e cists e=(L,a,g,T, l)EE s.t. u Eg, r→0ln,amdt'∈(1) wher'e Jor'd E R>o, u+d maps each clock a inl C to the value u(x)+d, and rHOu denotes the clock valuation uhich maps each clock in r to 0 and agrees with u over C\r Figure 2 illustrates the semantics of TA. From a given initial state, we can choose to takc an action or a delay transition(diffcrent valucs hcrc). Dcpcnding of the chosen delay, further actions may be forbidden Timed automata are often composed into a network of timed automata over a common set of clocks and actions, consisting of n timed automata A i L0,C,A,E,l),1≤i≤n. A location vector We compose the invariant functions into a common function over location vec- tors 1(0=Ailili). We write ll; / li to denote the vector where the ith element l i of l is rcplaccd by l;. In thc following we dcfinc the semantics of a nctwork of timed automata Definition 3(Semantics of a network of Timed Automata). Let A T a, O, C, A, Fi, Ii) be a network of n timed automata. Let lo=(49,., 19)be the initial location vector. The semantics is defined as a transition system(S,$0, -) where s=(L1x…×Ln)× r is the set of stales,so=(lo,to) is the initial state, and -C sxs is the transition relation defined by ,u)2(1,+a)wd:0≤d≤d→u+l∈ (,x)“,(ll,y) if there ccists l可l1st.u∈9, =p+0]uand'∈I(v/l]) (L, u)-(L[1/L,,/lil, u)if there exist li -li and 1lstu∈(9A91),v=p;Un0 u and u∈(1,l/1)口 As an exaIllple of the semantics, the lanp in Fig. 1 Imay have the follow ing states(we skip the user:(Lamp off, y=0)-(Lamp off, y= 3) 0)→(Lamp.1o,y=0.5)→(Lamp. bright,y=0.5 (Lamp bright, 3=1000) Timed Automata in Uppaal The UPPAAL modelling language extends timed automata with the following additional features(see Fig Templates automata are defined with a set of parameters that can be of any type(e.g, int, chan). These parameters are substituted for a given argument in the process declaration Constants are declared as const name value Constants by definition cannot be modified and must have an integer value Bounded integer variables are declared as int [min, max] name, where min and max are the lower and upper bound, respectively guards, invariants, and assignments may contain expressions ranging over bounded integer variables The bounds arc checked upon verification and violating a bound lcads to an invalid state that is discarded (at run-time). If the bounds are omitted, the default range of-32768 to 32768 is llsed rile Template p System Edit Simulator Verite Drag out 1c ier T1 catlon oT Eal arino τ ens b ostra1rtS01Wn Pettersson and Mats Dalie=. In Proceed- ngs of the /tr Interna ontererce on「 crirtion echni aes, pages 220-208, North-lloT1Erd. 1994 constant const N D,N:1 integer ∈的Ty:Y0一3℃y,h,ad0,「e勤 Drag out A Name: In Que. Parameters: Int, O, N]e Ice templates stem Drag out Name: Gate P arameters. o-a Gate channel canonisation Fig3. Declarations of a constant and a variable, and illustration of somc of the channel synchronisations between two templates of the train gate example of Section 1, and simle committed locations Binary synchronisation channels are declared as chan c. All edge labelled with c! synchronises with another labelled c?. A synchronisation pair is chosen non-deterministically if several combinations are enabled Broadcast channels are declared as broadcast chan c In a broadcast syn chronisation one sender c! can synchronise with an arbitrary number of rcccivcrs c?. Any rcccivcr than can synchronise in thc current statc must do sO. If there are no receivers, then the sender can still execute the c! action i.e. broadcast, sending is never blocking Urgent synchronisation channels are declared by prefixing the channel decla ration with the keyword urgent Delays must not occur if a synchronisation transition on an urgent channel is enabled. Edges using urgent channels for synchronisation cannot have time constraints, i. e, no clock guards Urgent locations are semantically equivalent to adding an extra clock x, that S reset on all incoming edges, and having an invariant x<=o on the location Hence, time is not allowed to pass when the system is in an urgent location Corrrnitted locations are even inore restrictive ol the execution than urgent LocatiOns. A state is cOInInitted if ally of the loca tions in the state is commit- ed a committed state cannot delay and the next transition must involye an outgoing edge of at least one of the committed locations Arrays are allowed for clocks, channels, constants and integer variables. They are defined by appending a size to the variable name, e.g. chan c[4]: clock a[2];int[3,5]u[7; Initialiscrs arc uscd to initialise integer variables and arrays of integer vari- ables. For instance, int i =2; or int i[3]=1 Record types are declared with the struct construct like in C Custom types are defined with the C-like typedef construct. You can define any custom-type from other basic types such as records User functions are defined either globally or locally to templates. Template parameters are accessible from local functions. The syntax is similar to C except that thcre is no pointer. C++ syntax for rcfcrcnccs is supported for the arguments only Expressions in U ppaal Expressions in UPPAAL range over clocks and integer ariables. The bnf is given in Fig. 33 in the appendix. Expressions are used with the following labels Select A select label contains a comma separated list of name: type expressions where name is a variable name and type is a defined type(built-in or custom) These variables are accessible on the associated edge only and they will take a llOll-deterlnlinistic value in the range of their respective types Guard a guard is a particular expression satisfying the following conditions it is side-effect free: it evaluates to a boolean: onlly clocks, integer variables and constants are referenced (or arrays of these types ) clocks and clock differences are only compared to integer expressions; guards over clocks are essentially conjunctions(disjunctions arc allowcd ovcr integer conditions). A guard may call a side-effect free function that returns a bool, although clock constraints are not supported in such functions Synchronisation A synchronisation label is either on the forIll E pression or Erpression? or is an empty label. The expression must be side-effect free evaluate to a channel, and only refer to integers, constants and channels Update An update labcl is a comma scparatcd list of exprcssions with a sidc expressions must only refer to clocks, integer variables, and constants and only assign integer values to clocks. They may also calI functions Invariant An invariant is an expression that satisfies the following conditions: it is side-effect free; only clock, integer variables, alld constants are referenced it is a conjunction of conditions of the form x<e or x<=e where x is a clock eference and e evaluates to an int all a side-effect fi function that returns a bool, although clock constraints arc not supported in such functions 2.2 The Query Language The main purpose of a model-checker is verify the model w.r. t. a requirement specification. Like the model, the requirement specification must be expressed in a formally well-defined and machine readable language. Several such logics exist in thc scicntific litcraturc, and UPPAAL uscs a simplified version of TCTL Like in TCTL, the query language consists of path formulae and state formulae. 2 State formulae describe individual states, whereas path formulae quantify over paths or traces of the model. Path formulae can be classified into reachability safety and liveness. Figure 4 illustrates the different path formulae supported by UPPAAL. Each type is described below State Formulae A state formula is an expression (see Fig. 33 ) that can be evaluated for a state without looking at the behaviour of the model. For instance this could be a simple expression, like i ==7, that is true in a state whenever equals 7. The syntax of state formulae is a superset of that of guards, i.e:a state formula is a side-effect free expression, but in contrast to guards. the use of disjunctions is not restricted. It is also possible to test whether a particular proccss is in a givcn location using an cxprcssion on the form P l, where P is a rocess and l is a location In UPPAAL, deadlock is expressed using a special state formula(although this is not strictly a state formula). The formula simply consists of the keyword deadlock and is satisfied for all deadlock states. a state is a deadlock state if there are no outgoing action transitions neither froin the state itself or any of its delay successors. Due to current limitations in UPPAAL, the deadlock state formula can only bc uscd with reachability and invariantly path formulac(scc Reachability Properties Reachability properties are the simplest form of properties. They ask whether a given state formula, f, possibly call be satisfied In contrast to TOTL, UPPAAL, does not allow nesting of path formulae Fig. 4. Path formulae supported in UPPAAL. The filled states are those for which a given state formulac o holds. Bold edges are uscd to show the paths the formulac evaluate on by any reachable statc. Anothcr way of stating this is: Docs thcrc exist a path starting at, the initial state, such that. p is eventually sa tisfied along that, path Reachability properties are often used while designing a Inodel to perforIn sanity checks. For instance, when creating a model of a communication protocol involving a scndcr and a rcccivcr, it makcs scnsc to ask whether it is possiblc for the sender to send a message at all or whether a message can possibly be received. These properties do not by themselves guarantee the correctness of the protocol (i.e. that any message is eventually delivered), but they validate the basic behaviour of the model We express that some state satisfying y should be reachable using the path formula Fo pp. In UPPAAL, we write this property using the syntax E<> P Safety properties Safety properties are on the form: "something bad will never happen". For instance, in a. model of a nuclear power plant, a safety property might be, that the operating temperature is always(invariantly) under a certain threshold, or that a meltdown never occurs. a variation of this property is that soillething will possibly never happen. For instance when playing a gaine. a safe state is one in which we can still win the game, hence we will possibly not loose Iu UPPaal these proper ties are formulated positivelv, e.g., SOInlething good s invariantly true. Let ie be a state formulae. We express that p should be true in all reachable states with the path formulae A口φp,3 whereas e口 says that Notice that all o--1◇vg there should exist a maximal path such that y is always true. 4 In UPPAAL we write AD] and E[] respectivel Liveness Properties Liveness properties are of the forIn: soMething will eveIl- tually happen, e.g. when pressing the on button of the remote control of the television, then eventually the television should turn on. Or in a model of a communication protocol, any mcssagc that has bccn scnt should eventually bc received In its simple form, liveness is expressed with the path formula. Ao 4, mean ing yp is eventually satisfied. The more useful form is the leads to or response property. written hich is read atisfied. then eventu ally y will be satisfied, e.g. whenever a Inlessage is sent, then eventually it will be received. In UPPAAL these properties are written as A<> and p -->l. rcspcctivcly 2.3 Understanding Time Invariants and Guards UPPAAL. llses a continuous time model. we illustrate the concept of time with a simple example that makes use of an observ mally an observer is an add-on automaton in charge of detecting events without changing the observed systelll. In our case the clock reset (x: =0) is delegated t he observer for illustration purposes Figure 5 shows the first model with its observer. We have two automata in parallel. The first automaton has a sclf-lool clock that synchronises on the channel reset with the second automaton the second automaton, the observer, detects when the self loop edge is taken with the locat d then has an edge going back to idle that resets the clock x. We unloved the reset of x froI the self loop to the observer only to test what happels on the transition before the reset. Notice that the location taken is committed (marked c)to avoid delay in that location The following propcrtics can be vcrificd in UPPAAL (scc scction 3 for an overview of the interface). Assuming we name the observer automaton Obs. we have A D Dbs taken imply x>=2: all resets off x will happen when x is above 2. This query Illealis that for all reachable states, being in the locatiOn Obs. taken implies that x>=2 E<> Obs. idle and x>3: this property requires, that it is possible to reach ablc statc whcrc Obs is in thc location idle and x is bigger than 3. esscntially we check that we may delay at least 3 time units between resets. The result would have been the same for larger values like 30000, since there are no invariants in this model A A maximal path is a path that is either infinite or where the last state has no outgoing transitions. Notice that a◇=-E囗-y 6 Experts in TCTL, will recognise that yp my i) is equivalent to An(-> A np) 9 (b)Observer c) Behaviour: one possible run Fig. 5. First example with an observer. (b)Updated behaviour with an invariant Fig. 6. Updated cxample with an invariant. The observer is the same as in Fig. 5 and s not shown here We update the first model and add an invariant to the location loop, as shown iIl Fig. 6. The invariant is a progress conditiOn: the systeln is not allowed to stay in the state more than 3 time units. so that the transition has to be taken and the clock reset in our example. Now the clock x has 3 as an upper bound. The following properties hold A[] Obs. taken imply (x>=2 and x<=3) shows that the transition is taken when x is between 2 and 3, i.e., after a delay between 2 and 3 E<> Obs. idle and x>2: it is possible to take the transition when x is be tween 2 and 3. The upper bound 3 is checked with the next propert A[] Obs. idle imply x<=3: to show that the upper bound is respected The formcr propcrty E<> Obs. idle and x>3 no longer holds Now, if we remove the invariant and change the guard to x>=2 and x<= you may think that it is the same as before, but it is not! The system has no progress condition, just a new condition on the guard. Figure 7 shows what appens: the systelll lllay take the saine transitions as before, but deadlock also occur. The system may be stuck if it does not take the transition after 3 time units. In fact, the system fails the property A[] not deadlock. The property A[] Obs. idle imply x<=3 does not hold any longer and the deadlock can also be illustrated by the property A[] x>3 imply not Obs. taken, i. e, after 3 time units, the transition is not ta ken any more

试读 48P UPPAAL建模工具教程(英文详细版)
立即下载 低至0.43元/次 身份认证VIP会员低至7折
UPPAAL建模工具教程(英文详细版) 39积分/C币 立即下载

试读结束, 可继续读5页

39积分/C币 立即下载 >