Kinh doanh - Marketing
Kinh tế quản lý
Biểu mẫu - Văn bản
Tài chính - Ngân hàng
Công nghệ thông tin
Tiếng anh ngoại ngữ
Kĩ thuật công nghệ
Khoa học tự nhiên
Khoa học xã hội
Văn hóa nghệ thuật
Sức khỏe - Y tế
Văn bản luật
Nông Lâm Ngư
Kỹ năng mềm
Luận văn - Báo cáo
Giải trí - Thư giãn
Tài liệu phổ thông
Văn mẫu
Tài liệu HOT
Tìm
Danh mục
Kinh doanh - Marketing
Kinh tế quản lý
Biểu mẫu - Văn bản
Tài chính - Ngân hàng
Công nghệ thông tin
Tiếng anh ngoại ngữ
Kĩ thuật công nghệ
Khoa học tự nhiên
Khoa học xã hội
Văn hóa nghệ thuật
Y tế sức khỏe
Văn bản luật
Nông lâm ngư
Kĩ năng mềm
Luận văn - Báo cáo
Giải trí - Thư giãn
Tài liệu phổ thông
Văn mẫu
Thông tin
Điều khoản sử dụng
Quy định bảo mật
Quy chế hoạt động
Chính sách bản quyền
0
Trang chủ
Công Nghệ Thông Tin
Kỹ thuật lập trình
Lecture Formal methods in software engineering: A transition system
Đang chuẩn bị liên kết để tải về tài liệu:
Lecture Formal methods in software engineering: A transition system
Quốc Hiền
96
63
pptx
Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
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.e., I (s0). Moving from one state si to its successor si+1 is by executing a transition e t: e (si), i.e., 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.e., I (s0). Moving from one state si to its successor si+1 is by executing a transition e t: e (si), i.e., si satisfies e. si+1 is obtained by applying t to si. 4 13 5 Example: s0= s1= s2= s3=
TÀI LIỆU LIÊN QUAN
Lecture Formal methods in software engineering: What are formal methods?
Lecture Formal methods in software engineering: Formal methods
Lecture Formal methods in software engineering: What are formal methods?
Lecture Formal methods in software engineering: Formal methods
Lecture Formal methods in software engineering: Formal specification
Lecture Formal methods in software engineering: Formal specification
Lecture Formal methods in software engineering - Lecture 9: Formal methods
Lecture Formal methods in software engineering - Lecture 9: Formal methods
Lecture note Formal methods in software engineering - Lecture 2: Formal languages (cont)
Lecture note Formal methods in software engineering - Lecture 2: Formal languages (cont)
Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.