时间自动机课件.ppt

1、2008 -12-151n The theory of Timed automatan A case study2008 -12-152nFirst introduced by Rajeev Alur and David L. Dill in 1990,nRajeev Alur and David L. Dill. Automata for modeling real-time systems. In Proceedings, 17th International Colloquium on Automata, Languages and Programming, 1990.nR. Alur

2、and D. L. Dill.: A theory of timed automata In Theoret. Comput. Sci., Vol. 126, No.2, 1994, pp. 183-235nA finite-state Buchi automaton extended with a set of real value variablesnTimed safety automata 2008 -12-153OffLightBrightPressPressPressPressWANT: if press is issued twice quickly then the light

3、 will get brighter; otherwise the light is turned off.2008 -12-154OffLightBrightSolution: Add a real-valued clock x x:=0 x3PressPressPressPressAdding continuous variables to state machines2008 -12-155nmaClocks: x, yx3x := 0Guard Boolean combination of comparisons withInteger/rational boundsResetActi

4、on performed on clocks( n , x=2.4 , y=3.1415 ) ( n , x=3.5 , y=4.2415 )wait(1.1)Transitions( n , x=2.4 , y=3.1415 ) ( m , x=0 , y=3.1415 )aState ( location , x=v , y=u ) where v,u are in RAction for synchronization2008 -12-156nmaClocks: x, yx3x := 0Transitions:( n , x=2.4 , y=3.1415 ) ( n , x=3.5 ,

5、y=4.2415 ) wait(1.1)( n , x=2.4 , y=3.1415 ) wait(3.2)x=5y(l,v+d) if both v and v+d satisfy I(l)q Location switch transitions: (l,v)-a-(l,v) if there is an edge (l,a,g,l,l) such that v satisfies g and v=vl:=02008 -12-159n The product of automata n We use timed automata network to model them2008 -12-

6、1510ABx3aba |a,x:=0abcCDy3bb|b,y:=0bcACBCx3ab, y:=0a|a,x:=0ADy3cBDx4y3, b|x3, b,y:=0a|a, x:=0y3ca, x:=02008 -12-1511q System modeled as timed automata networksq Properties specified as CTL formulars.q Verification problem reduced to reachability or to temporal logic model checkingq ApplicationsReal-

7、time controllersAsynchronous timed circuitsSchedulingDistributed timing-based algorithms2008 -12-1512specification of the goal系统需求系统需求现实现实environmentPLC programPLCfulfils2008 -12-1513specification of the environmentspecification of the control系统规范系统规范结构描述结构描述 plant diagramPLC programspecification of

8、 the goal系统需求系统需求automaton for the plantautomaton for the program2008 -12-1514specification of the goal系统需求系统需求automaton for the plantautomaton for the programT_plant | T_program |= Property模型检测：模型检测：2008 -12-1515n Steeve controller : Part of a theater machinery control system n Steeve uused for pul

9、ling light and screen, ucan move up and down, located at any preset height,upowered by motor.uRange 15-195n Control modeuAutomatic: given the target height, the steeve achieve automaticlly. uManual: user can let the steeve move up, down and stop 2008 -12-15162008 -12-1517n In natural languageuThe st

10、eeve stops at the required height.uThe steeve must move under the safety range, cannot exceed the upper and lower bounds.uMake sure the whole operation can be finished within 60s.2008 -12-1518n 9 signals are defined for synchronization, they are stop, start, up, down, impulse, inc, cw, acw and sp.n

11、One signal is shared by two components for their synchronization n The relationship of the height and the impulse number is:uimpulse_number = height * 2n 1 time unit is 0.01s2008 -12-1519n Finite automatan a=1: automatic mode. n a=0 : manual mode n If we want to simulate a sequence of operations, ca

12、n be modeled as TA2008 -12-1520nmotor with fixed speednsensor issues an impulse every 2 time units.nConstrain formula y=2 belongs to I(rt_acw)nCyclic transition, y is reset to 0, signal impulse is issued every two time unites until stop order sp is received2008 -12-1521nThere is time delay between s

13、ensor receiving impulse and sending inc to controller.nThe delay is below 1 time unite.nClock variable x is used to represent the time delay.2008 -12-1522nFunctionuCmp, convert, unhigh, nlow, chnVariablesuh_req: required heightuh_curr: current heightum target counting number un current counting numb

14、er 2008 -12-1523n 8 traces, half for rising up, half for falling down.n Automatic modeuUser gives a required height, the steeve reaches there. (0,3,5,7,0)uBefore reaching there, user suddenly stop it.(0,3,5,8,0)n Manuel modeuPress up, later press stop. (0,1,5,8,0)uForget to press stop, when reach th

15、e bound, motor is forced to stop. (0,1,5,10,0)2008 -12-1524n Use tool UppaaluA timed automata verification tool n Properties descriptionuA simplied version of CTL : temporal operators are F() and G()2008 -12-1525nthe system should be deadlock freeuA not deadlocknIn the automatic mode, when the user

16、sets the required height, the steeve should eventually reach the target position.uA a=1 imply (h_curr=h_req)nthe steeve never extend the upper and lower bounduA 15=h_curr=195nWhen the steeve reaches the required height, the motor should have stopped.uA (a=1 and h_req=h_curr) imply motor.static2008 -

17、12-1526n The accumulated time that the steeve reaches the required height should below 6000 time unitsuA clock variable k and a boolean variable d are neededuA controller.d=1 imply (controller.k=6000)n In the manual mode, when the stop order is issued by user, the motor will stop within 2 time units.uA (not a=0 and c=1 ) imply u=22008 12 - 1527精品课件精品课件！2008 12 - 1528精品课件精品课件！2008 -12-1529 Any question ?