Lecture Formal methods in software engineering: A transition system

In this chapter, the following content will be discussed: A transition system, the interleaving model, the transitions, some important points, interleaving semantics: execute one transition at a time, interleaving semantics, busy waiting, combinatorial explosion, properties of formalisms,. | 1 Formal Methods in SE Qaisar Javaid Assistant Professor Lecture # 10 2 A transition system A (finite) set of variables V over some domain. A set of states S. A (finite) set of transitions T, each transition e t has an enabling condition e, and a transformation t. An initial condition I. 2 11 3 Example V={a, b, c, d, e}. S: all assignments of natural numbers for variables in V. T={c >0 (c,e):=(c -1,e +1), d >0 (d,e):=(d -1,e +1)} I: c =a /\ d =b /\ e =0 What does this transition system do? 3 12 4 The interleaving model An execution is a maximal finite or infinite sequence of states s0, s1, s2, That is: finite if nothing is enabled from the last state. The first state s0 satisfies the initial condition, ., I (s0). Moving from one state si to its successor si+1 is by executing a transition e t: e (si), ., si satisfies e. si+1 is obtained by applying t to si. 4 13 5 Example: s0= s1= s2= s3= T={c>0 (c,e):=(c -1,e +1), d>0 (d,e):=(d-1,e+1)} I: c=a /\ d=b /\ e=0 5 14 6 L0:While True do NC0:wait(Turn=0); CR0:Turn=1 endwhile || L1:While True do NC1:wait(Turn=1); CR1:Turn=0 endwhile T0:PC0=L0 PC0:=NC0 T1:PC0=NC0/\Turn=0 PC0:=CR0 T2:PC0=CR0 (PC0,Turn):=(L0,1) T3:PC1=L1 PC1=NC1 T4:PC1=NC1/\Turn=1 PC1:=CR1 T5:PC1=CR1 (PC1,Turn):=(L1,0) Initially: PC0=L0/\PC1=L1 The transitions Is this the only reasonable way to model this program? 6 17 7 The state graph:Successor relation between reachable states. Turn=0 L0,L1 Turn=0 L0,NC1 Turn=0 NC0,L1 Turn=0 CR0,NC1 Turn=0 NC0,NC1 Turn=0 CR0,L1 Turn=1 L0,CR1 Turn=1 NC0,CR1 Turn=1 L0,NC1 Turn=1 NC0,NC1 Turn=1 NC0,L1 Turn=1 L0,L1 T0 T0 T3 T3 T1 T4 T3 T0 T3 T0 T0 T4 T1 T3 T2 T2 T5 T5 7 18 8 Some important points Reachable states: obtained from an initial state through a sequence of enabled transitions. Executions: the set of maximal paths (finite or terminating in a node where nothing is enabled). Nondeterministic choice: . | 1 Formal Methods in SE Qaisar Javaid Assistant Professor Lecture # 10 2 A transition system A (finite) set of variables V over some domain. A set of states S. A (finite) set of transitions T, each transition e t has an enabling condition e, and a transformation t. An initial condition I. 2 11 3 Example V={a, b, c, d, e}. S: all assignments of natural numbers for variables in V. T={c >0 (c,e):=(c -1,e +1), d >0 (d,e):=(d -1,e +1)} I: c =a /\ d =b /\ e =0 What does this transition system do? 3 12 4 The interleaving model An execution is a maximal finite or infinite sequence of states s0, s1, s2, That is: finite if nothing is enabled from the last state. The first state s0 satisfies the initial condition, ., I (s0). Moving from one state si to its successor si+1 is by executing a transition e t: e (si), ., si satisfies e. si+1 is obtained by applying t to si. 4 13 5 Example: s0= s1= s2= s3=