南京大学：《嵌入式网络物理系统》课程教学资源（PPT讲稿）时光自动机 Timed Automata

大房 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