时间自动机课件.ppt

Outline,The theory of Timed automataA case study,First introduced by Rajeev Alur and David L.Dill in 1990,Rajeev Alur and David L.Dill.Automata for modeling real-time systems.In Proceedings,17th International Colloquium on Automata,Languages and Programming,1990.R.Alur and D.L.Dill.:A theory of timed automata In Theoret.Comput.Sci.,Vol.126,No.2,1994,pp.183-235A finite-state Buchi automaton extended with a set of real value variablesTimed safety automata,Off,Light,Bright,Press,Press,Press,Press,WANT:if press is issued twice quickly then the light will get brighter;otherwise the light is turned off.,Simple Light Control,Simple Light Control,Off,Light,Bright,Solution:Add a real-valued clock x,x:=0,x=3,x3,Press,Press,Press,Press,Adding continuous variables to state machines,Timed Automata,n,m,a,Clocks:x,y,x3,x:=0,Guard Boolean combination of comparisons withInteger/rational bounds,ResetAction performed on clocks,State(location,x=v,y=u)where v,u are in R,Action for synchronization,n,m,a,Clocks:x,y,x3,x:=0,Transitions:,(n,x=2.4,y=3.1415)(n,x=3.5,y=4.2415),wait(1.1),(n,x=2.4,y=3.1415),wait(3.2),x=5,y=10,LocationInvariants,g1,g2,g3,g4,Invariants ensure progress!,Adding Invariants,Timed Automata：Syntax,Timed Automata:a tuple(L,l0,A,V,I,E)L:a finite set of locationsl0:initial locationsA:a finite set of labels(alphabet)V:a finite set of clock variablesI:a location constrain functionE:a finite set of edges.Each edge hasa source location l,a target location lGuard g(variable constrain)Label a in A(e labels also allowed)A subset u of clock variables to be reset,Timed Automata:Semantics,For a timed automaton A,define an infinite-state transition system S(A)States Q:a state q is a pair(l,v),where l is a location,and v is a clock vector,mapping clocks in X to R+,satisfying I(l)(l0,v)is initial state if l is in V0 and v(x)=0 Elapse of time transitions:for each nonnegative real number d,(l,v)-d-(l,v+d)if both v and v+d satisfy I(l)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:=0,Parallel Composition,The product of automata We use timed automata network to model them,Product Construction,Verification,System modeled as timed automata networks Properties specified as CTL formulars.Verification problem reduced to reachability or to temporal logic model checking ApplicationsReal-time controllersAsynchronous timed circuitsSchedulingDistributed timing-based algorithms,specification of the goal,系统需求,现实,environment,PLC program,PLC,fulfils,Verification goal,specification of the environment,specification of the control,系统规范,结构描述,plant diagram,PLC program,Model checking,specification of the goal,系统需求,automaton for the plant,automaton for the program,Model checking,specification of the goal,系统需求,automaton for the plant,automaton for the program,T_plant|T_program|=Property,模型检测：,A PLC Control System In Theater,Steeve controller:Part of a theater machinery control system Steeve used for pulling light and screen,can move up and down,located at any preset height,powered by motor.Range 15-195Control modeAutomatic:given the target height,the steeve achieve automaticlly.Manual:user can let the steeve move up,down and stop,Structure of Steeve Control System,Requirements,In natural languageThe steeve stops at the required height.The steeve must move under the safety range,cannot exceed the upper and lower bounds.Make sure the whole operation can be finished within 60s.,Modeling by timed automata,9 signals are defined for synchronization,they are stop,start,up,down,impulse,inc,cw,acw and sp.One signal is shared by two components for their synchronization The relationship of the height and the impulse number is:impulse_number=height*21 time unit is 0.01s,User Automaton,Finite automataa=1:automatic mode.a=0:manual mode If we want to simulate a sequence of operations,can be modeled as TA,Motor Automaton,motor with fixed speedsensor issues an impulse every 2 time units.Constrain formula y=2 belongs to I(rt_acw)Cyclic transition,y is reset to 0,signal impulse is issued every two time unites until stop order sp is received,Sensor Automaton,There is time delay between sensor receiving impulse and sending inc to controller.The delay is below 1 time unite.Clock variable x is used to represent the time delay.,Controller Automaton,FunctionCmp,convert,nhigh,nlow,chVariablesh_req:required heighth_curr:current heightm target counting number n current counting number,Controller traces,8 traces,half for rising up,half for falling down.Automatic modeUser gives a required height,the steeve reaches there.(0,3,5,7,0)Before reaching there,user suddenly stop it.(0,3,5,8,0)Manuel modePress up,later press stop.(0,1,5,8,0)Forget to press stop,when reach the bound,motor is forced to stop.(0,1,5,10,0),Property verification,Use tool UppaalA timed automata verification tool Properties descriptionA simplied version of CTL:temporal operators are F()and G(),Property verification,the system should be deadlock freeA not deadlockIn the automatic mode,when the user sets the required height,the steeve should eventually reach the target position.A a=1 imply(h_curr=h_req)the steeve never extend the upper and lower boundA 15=h_curr=195When the steeve reaches the required height,the motor should have stopped.A(a=1 and h_req=h_curr)imply motor.static,Time bounded property verification,The accumulated time that the steeve reaches the required height should below 6000 time unitsA clock variable k and a boolean variable d are neededA controller.d=1 imply(controller.k=6000)In the manual mode,when the stop order is issued by user,the motor will stop within 2 time units.A(not a=0 and c=1)imply u=2,精品课件！,精品课件！,Thanks,Any question?,