Tiểu Luận Tìm hiểu erigone model checker

MỤC LỤC
LỜI NÓI ĐẦU. 1
Chương 1. ERIGONE TRÊN CÔNG CỤ EUI 2
I/ Giới thiệu tổng quan. 2
1. Giới thiệu Erigone model checker 2
2. Công cụ phát triển. 3
2.1. Command line. 3
2.2. EUI (Erigone User Interface) 6
3. Mô phỏng và xác minh trong Erigone. 8
4. Chương trình Trace. 9
II/ Ví dụ demo. 10
1. Giải quyết hai tiến trình loại trừ lẫn nhau. 10
2. Loại trừ lẫn nhau với một semaphore. 11
3. Xác minh một chương trình Promela với câu lệnh assert 13
4. Xác minh một thuộc tính an toàn sử dụng LTL. 14
5. Chứng minh khái niệm về sự công bằng với câu lệnh LTL. 16
Chương 2: ERIGONE BẰNG CÂU LỆNH. 20
I/ Tìm hiểu về Erigone bằng dòng lệnh: 20
1. Erigone: 20
1.1. Thực thi theo phương thức: 21
1.2. Hiển thị lựa chọn với các đối số: 22
1.3. Biên dịch chạy thông điệp: 22
1.4. Chuyển tiếp(transitions): 22
1.5. Chuyển đổi LTL: 23
1.6. Kiểm tra lỗi(debug arguments) 23
2. List: 24
3. Trace: 24
4. VMC 25
II/ Mô phỏng một số chương trình Promela bằng công cự Erigone. 26
1. Mô phỏng với quá trình truyền thông điệp(chanel) 26
2. Mô phỏng chương trình tương tranh. 33
3. Kiểm chứng độ tin cậy khi sử dụng LTL. 34
III/ Chương trình List 35
IV/ Chương trình Trace. 35
V/ Chương trình VMC 38
TÀI LIỆU THAM KHẢO. 42



LỜI NÓI ĐẦU Erigone là mô hình triển khai lại của mô hình kiểm chứng Spin được phát triển với mục đích kiểm chứng được dễ dàng trực quan, uyển chuyển nhằm thuận lợi cho việc nghiên cứu và mô phỏng mô hình hệ thống, erigone có thể được thực hiện bằng công cụ trên giao diện đồ họa EUI hoặc thao tác bằng câu lệnh dưới dạng command line với nhiều tùy biến lựa chọn cho phép kiểm chứng hoạt động của hệ thống.
Tìm hiểu Erigone model checker nhằm mục đích tìm hiểu rõ hơn về mô hình kiểm chứng erigone thông qua một số ví dụ, được thực hiện bằng công cụ đồ họa EUI và bằng câu lệnh command line, với những nhìn ảnh, phân tích chương trình một cách trực quan.
Vì đây là lần đầu tiếp xúc, tìm hiểu về 1 khía cạnh mới nên sẽ không tránh khỏi những khó khăn dẫn đến những thiếu sót trong báo cáo, chúng em mong thầy (cô) bỏ qua.
Chúng em xin chân thành cảm ơn thầy cô đã chỉ bảo hướng dẫn chúng em để chúng em có thể hoàn thành báo cáo này.