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.
   

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

2. 
   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.
   

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