Timed Automata, Timed Computation Tree Logic and CTL Models for Real Time Systems.

Timed Automata, Timed Computation Tree Logic and CTL Models for Real Time Systems.

In this talk, Paul Pettersson from BRICS Aalborg discusses timed automata and timed computation tree logic as formalisms for modeling

  • Uploaded on | 3 Views
  • beth beth

About Timed Automata, Timed Computation Tree Logic and CTL Models for Real Time Systems.

PowerPoint presentation about 'Timed Automata, Timed Computation Tree Logic and CTL Models for Real Time Systems.'. This presentation describes the topic on In this talk, Paul Pettersson from BRICS Aalborg discusses timed automata and timed computation tree logic as formalisms for modeling. The key topics included in this slideshow are . Download this presentation absolutely free.

Presentation Transcript

Slide1Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata and Timed Computation Tree Logic Paul Pettersson BRICS@Aalborg

Slide2Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. CTL Models = Kripke Structures

Slide3Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Computation Tree Logic, CTL Clarke & Emerson 1980 Syntax

Slide4Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. CTL, Derived Operators . . . . . . . . . . . . p p p AF p . . . . . . . . . . . . p EF p possible inevitable ”exists eventually” or ”reachable” ”exists globally”

Slide5Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. CTL, Derived Operators p p p . . . . . . . . . . . . AG p p p p p p p . . . . . . . . . . . . EG p p always potentially always for all paths next ”forall globally” or ”invariantly” ”forall eventually”

Slide6Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 18

Slide7Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide8Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide9Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide10Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide11Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide12Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide13Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide14Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide15Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. 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. Timed Automata Intelligent Light Control

Slide16Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata Intelligent Light Control Off Light Bright Solution:  Add real-valued clock   x X:=0 X<=3 X>3 press? Press? press? Press?

Slide17Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata n m a (Alur & Dill 1990) Clocks :    x, y x<=5 & y>3 x := 0 Guard Boolean combination of comp with integer bounds Reset Action perfumed on clocks Transitions (   n  ,  x =2.4 ,  y =3.1415  )                                   (   n  ,  x =3.5 ,  y =4.2415  ) e(1.1) (   n  ,  x =2.4 ,  y =3.1415  )                                   (   m  ,  x =0 ,  y =3.1415  ) a State    (   location  ,  x =v ,  y =u  )     where v,u are in  R Action used for synchronization

Slide18Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. n m a Clocks:    x, y x<=5 & y>3 x := 0 Transitions (   n  ,  x =2.4 ,  y =3.1415  )                                   (   n  ,  x =3.5 ,  y =4.2415  )             e(1.1) (   n  ,  x =2.4 ,  y =3.1415  )         e(3.2) x<=5 y<=10 Location Invariants g1 g2 g3 g4  Invariants ensure progress!! Timed Safety Automata = Timed Automata + Invariants (Henzinger et al, 1992)

Slide19Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Clock Constraints

Slide20Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed (Safety) Automata

Slide21Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example guard reset location

Slide22Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example guard reset location

Slide23Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide24Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide25Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide26Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide27Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Light Switch push push click

Slide28Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Light Switch • Switch may be turned on whenever at least 2 time units has elapsed since last “turn off” push push click

Slide29Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Light Switch • Switch may be turned on whenever at least 2 time units has elapsed since last “turn off” • Light automatically switches off after 9 time units. push push click

Slide30Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Semantics • clock valuations : • state : • Semantics of timed automata is a  labeled transition system where • action transition • delay Transition g  a  r l l’

Slide31Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Semantics: Example push push click

Slide32Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Networks of Timed Automata  + Integer Variables + arrays …. l1 l2 a! x>=2 i==3 x := 0 i:=i+4 m1 m2 a? y<=4       …………. Two-way synchronization on  complementary  actions. Closed Systems! ( l1 ,  m1 ,………, x=2, y=3.5, i=3,…..)              ( l2,m2 ,……..,x=0,  y=3.5, i=7,…..)  ( l1,m1 ,………,x=2.2, y=3.7, I=3,…..) 0.2 tau Example transitions If   a   URGENT CHANNEL

Slide33Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata in U PPAAL • Timed Safety Automata + urgent actions + urgent locations    (i.e. zero-delay locations) + committed locations    (i.e. zero-delay and  atomic  locations) + data-variables (integers with bounded domains) + arrays of data-variables + guards and assignments over data-variables and    arrays...

Slide34Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Urgent and Committed Locations m n o p q r 2.5 a committed urgent d d

Slide35Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. TCTL = CTL + Time constraints over formula clocks and automata clocks “freeze operator” introduces new formula clock z E[   U   ], A[   U    ]  - like in CTL No  EX  

Slide36Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Derived Operators Along any path   holds continuously until within 7 time units  becomes valid. = = The property   becomes valid within 5 time units.

Slide37Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Paths Example: push push click

Slide38Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Elapsed time in path Example:  

Slide39Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. TCTL Semantics s  - location w  - formula clock valuation P M ( s ) - set of paths from  s Pos (  ) - positions in    ,i) - elapsed time  (i,d) <<(i’,d’) iff (i<j) or ((i=j) and (d<d’))

Slide40Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timeliness Properties receive(m)  occurs within 5 time units after  send(m) receive(m)  occurs exactly 11 time units after  send(m) putbox  occurs periodically (exactly) every 25 time units (note: other  putbox ’s may occur in between)