Luận Văn Tìm hiểu bộ kiểm chứng mô hình Spin

MỤC LỤC
MỤC LỤC . 1
LỜI CẢM ƠN . 4
GIỚI THIỆU 5
ĐặT VấN Đề . 5
CấU TRÚC KHÓA LUậN . 6
CHƯƠNG 1:KIỂM CHỨNG MÔ HÌNH 7
1. 1 KIểM CHứNG MÔ HÌNH 7
1. 2 CÁCH TIếN HÀNH 9
Các bước thực hiện của kiểm chứng mô hình. 10
Ưu nhược điểm của kiểm chứng mô hình. 10
Bên cạnh đó kiểm chứng mô hình cũng có những nhược điểm: . 11
CHƯƠNG 2:NGÔN NGỮ PROMELA . 12
2. 1 NGÔN NGữ PROMELA . 12
2. 1. 1 Cấu trúc chương trình Promela . 12
2. 1. 2 Kiểu dữ liệu cơ bản . 13
2. 1. 3 Toàn tử cơ bản 14
2. 1. 4 Tên, Tên hằng số và Biểu thức . 15
2. 1. 5 Tiến trình . 15
2. 2 Xử LÝ KÊNH TRONG PROMELA 16
2. 2. 1 Cú pháp . 16
2. 2. 2 Kênh gửi và nhận 16
2. 3. CÁC CÚ PHÁP . 17
2. 3. 1 Lệnh printf( ) . 17
2. 3. 2 Lệnh lựa chọn if 17
2. 3. 3 Lệnh lặp do 17
2. 3. 4 Lệnh nhảy goto 18
2. 3. 5 Lệnh define . 18
2. 4. RUN VÀ ATOMIC . 18
2. 4. 1 run và tiến trình init() 18
2. 4. 2 atomic 19
2
CHƯƠNG 3 BỘ KIỂM CHỨNG MÔ HÌNH 21
3. 1 Bộ KIểM CHứNG MÔ HÌNH SPIN . 21
3. 1. 1 Giới thiệu về SPIN 21
3. 1. 2 Công cụ jSPIN 21
3. 2. 3 Công cụ ISPIN 23
3. 2 DÙNG SPIN Đễ KIểM CHứNG . 25
3. 2. 1 Giả lập ngẫu nhiên 25
3. 2. 2 Verify 25
3. 3 GIớI THIệU Về LTL(LINEAR TEMPORAL LOGIC) 27
3. 3. 1 Cú pháp . 28
3. 3. 2 Ngữ nghĩa 29
CHƯƠNG 4 THỰC NGHIỆM . 31
4. 1 MÔ HÌNH MÁY TRạNG THÁI HƯU HạN 31
4. 2 THựC NGHIệM VớI Hệ THốNG ĐÈN . 31
4. 2. 1 MÔ Tả BÀI TOÁN 31
4. 2. 2 Kiểm chứng mô hình hệ thống đèn bắng SPIN 34
4. 2. 3 Bảng chuyển Atomata . 39
KẾT LUẬN . 40
 KếT QUả CủA KHÓA LUậN 40
 HƯớNG NGHIÊN CứU TIếP THEO . 40
TÀI LIỆU THAM KHẢO . 41
DANH SÁCH HÌNH ẢNH:
Hình1.1 Sơ đồ về việc kiểm chứng hệ thống . 8
Hình1.2 Sơ đồ hoạt động của phương pháp kiểm chứng mô hình 10
Hình3.1 Giao diện JPIN . 22
Hình3.2 Giao diện ISPIN . 23
Hình4.3 Cửa sổ của Verification 24
Hình3.4 Của sổ chạy chức năng View SPIN Atomaton 24
Hình4.1 Mô hình công tắc đèn . 32
3
Hình4.2 Kết quả chạy giả lập mô hình hệ thống đèn . 34
Hình4.3 JSPIN dịch từ LTL sang Promela 35
Hình4.4 Kết quả kiểm tra mô hình hệ thống đèn . 36
Hình4.5 Mô hình công tắc đèn không đúng . 37
Hình4.6 Kết quả kiểm chứng mô hình hệ thống đèn không thỏa mãn 39
Hình4.7 Kết quả bảng chuyển Atomata . 39