TAILIEUCHUNG - 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
đang nạp các trang xem trước
