大房 NANJING UNIVERSITY Timed automata
Timed Automata
Aim of the lecture knowledge of a basic formalism for modeling timed systems basic understanding of verification algorithms for timed systems(useful for practical modeling and verification)
Aim of the Lecture ◼ knowledge of a basic formalism for modeling timed systems ◼ basic understanding of verification algorithms for timed systems (useful for practical modeling and verification)
A Example: Peterson's Algorithm flaglo], flagll] (initialed to false)-meaning /want to access Cs turn (initialized to 0)-used to resolve conflicts Process o Process 1 while(true)( while(true) flag[o]: =true flag 1: true turn =0 while flag[l] and while flago and turn=I do) turn=0 dod; flag[0: false flag1: false
Example: Peterson's Algorithm ◼ flag[0], flag[1] (initialed to false) — meaning I want to access CS ◼ turn (initialized to 0) — used to resolve conflicts Process 0: while (true) { ; flag[0] := true; turn := 1; while flag[1] and turn = 1 do { }; ; flag[0] := false; } Process 1: while (true) { ; flag[1] := true; turn := 0; while flag[0] and turn = 0 do { }; ; flag[1] := false; }
AA Example: Peterson's Algorithm flag[o]: =1 NC W1 flag[0]: =0 tum: =1 flag[1==0 or turn==2 CS W2
Example: Peterson's Algorithm
A Example: Peterson's Algorithm )(岛 [1,1,1] n,1.1
Example: Peterson's Algorithm
Fischer's protocol id- shared variable each process has it's own timer(for delaying) for correctness it is necessary that K2> Kl Pr rocess 1 while(true) while id!=0 do i delay kl id delay k2 if (id=i d:=0
Fischer's Protocol ◼ id — shared variable ◼ each process has it's own timer (for delaying) ◼ for correctness it is necessary that K2 > K1 Process i: while (true) { ; while id != 0 do {} delay K1; id := i; delay K2; if (id = i) { ; id := 0; } }
Modeling real Time systems ■ Two models of time o discrete time domain o continuous time domain
Modeling Real Time Systems ◼ Two models of time: discrete time domain continuous time domain
Discrete Time domain a clock ticks at regular interval at each tick something may happen between ticks -the system only waits
Discrete Time Domain ◼ clock ticks at regular interval ◼ at each tick something may happen ◼ between ticks — the system only waits
Discrete Time domain choose a fixed sample period 8 all events happen at multiples of e simple extension of classical models ■ main disadvantage— how to choose? obig→ too coarse model o low 8= time fragmentation, too big state space usage: particularly synchronous systems(hardware circuits
Discrete Time Domain ◼ choose a fixed sample period ε ◼ all events happen at multiples of ε ◼ simple extension of classical models ◼ main disadvantage — how to choose ε ? big ε too coarse model low ε time fragmentation, too big state space ◼ usage: particularly synchronous systems (hardware circuits)
Continuous time domain time is modeled as real numbers delays may be arbitrarily small more faithful model, suited for asynchronous systems uncountable state space = cannot be directly handled automatically by brute force
Continuous Time Domain ◼ time is modeled as real numbers ◼ delays may be arbitrarily small ◼ more faithful model, suited for asynchronous systems ◼ uncountable state space cannot be directly handled automatically by “brute force