Bài tập lớn số 2 Môn: Formal Methods



tải về 6.26 Kb.
Chuyển đổi dữ liệu13.08.2016
Kích6.26 Kb.
Bài tập lớn số 2

Môn: Formal Methods

===============================================================

Hướng dẫn:

1. Deadline: trước 17:00, Ngày 30 tháng 8 năm 2010

2. Với mỗi thuộc tính, hãy viết các file proof score trình bày quá trình chứng minh thuộc tính giống như ví dụ mẫu đã trình bày trên lớp (trong file QLOCK.zip trên website) và nén thành một file .zip

3. Gửi báo cáo qua email:

• Gửi mail tới hungpn@vnu.edu.vn

• Subject của email là “[FM report2]”.

• CC cho bản thân để phòng trường hợp GV không nhận được mail (cần

giải trình).

===============================================================

Nội dung bài tập:

Dựa vào đặc tả QLOCK như đã cung cấp ở bài giảng số 8 và quá trình chứng minh thuộc tính inv1 như đã trình bày trên lớp, hãy chứng minh các thuộc tính sau luôn luôn đúng tại mọi trạng thái của hệ thống.



  1. Thuộc tính inv2: Với mọi agent I, tại mọi trạng thái S, nếu nhãn của I là cs (I đang sử dụng tài nguyên dùng chung) thì I phải ở top của hàng đợi tại trạng thái S.

Đặc tả của thuộc tính này trong CafeOBJ như sau:

eq inv2(S,I) = (pc(S,I) = cs implies top(queue(S)) = I) .




  1. Thuộc tính inv3: Với mọi agent I, tại mọi trạng thái S, nếu nhãn của I là wt thì I phải nằm trong hàng đợi tại trạng thái S.

Đặc tả của thuộc tính này trong CafeOBJ như sau:

eq inv3(S,I) = ((pc(S,I) = wt) implies (I in queue(S))) .


Chú ý: “in” là một phép toán chưa được định nghĩa trong qlock.mod. Các bạn phải định nghĩa nó và bổ sung vào qlock.mod.
==========================HẾT==========================


Cơ sở dữ liệu được bảo vệ bởi bản quyền ©hocday.com 2016
được sử dụng cho việc quản lý

    Quê hương