大房 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) <noncritical section <noncritical section> flag[o]: =true flag 1: true turn =0 while flag[l] and while flago and turn=I do) turn=0 dod; <critical section> <critical section> 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) { <noncritical section>; flag[0] := true; turn := 1; while flag[1] and turn = 1 do { }; <critical section>; flag[0] := false; } Process 1: while (true) { <noncritical section>; flag[1] := true; turn := 0; while flag[0] and turn = 0 do { }; <critical section>; 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