Đồ Án Nghiên cứu về kiểm chứng phần mềm sử dụng công cụ SPIN

Mục Lục








1 Mở đầu


1.1. Đặt vấn đề . 6


1.2. Mục tiêu và phạm vi của đề tài 7


1.3. Cấu trúc khóa luận 7


2 Sơ lược về Model Checking


2.1. Kiểm chứng hệ thống 8


2.2. Model Checking 9


2.2.1. Phương pháp hình thức và Model Checking 9


2.2.2. Hoạt động của Model Checking 9


2.2.3. Ưu nhược điểm của Model Checking 10


3 Ngôn ngữ Promela


3.1. Kiểu dữ liệu và toán tử cơ bản 13


3.1.1. Kiểu dữ liệu cơ bản .13


3.1.2. Toán tử cơ bản .13


3.2. Dữ liệu kiểu kênh trong Promela .14


3.2.1. Cú pháp .14


3.2.2. Kênh gặp (rendezvous channel) .15


3.3. Các cú pháp 15


3.3.1. Lệnh printf() 15


3.3.2. Lệnh lựa chọn if .15


3.3.3. Lệnh lặp do .16


3.3.4. Lệnh nhảy goto 16





3.3.5. Lệnh define .16


3.4. run và atomic 17


3.4.1. run và tiến trình init() .17


3.4.2. atomic .17


4 Kiểm chứng chương trình trong Spin


4.1. Kiểm chứng chương trình trong Spin 20


4.1.1. Giả lập ngẫu nhiên 20


4.1.2. Verify 22


4.2. Logic thời gian tuyến tính (LTL) .24


4.2.1. Cú pháp 25


4.2.2. Biểu diễn tính chất bất biến của hệ thống bằng LTL .26


4.3. Cấu trúc Never Claim .26


5 Thực nghiệm


5.1. Mô hình máy hữu hạn trạng thái .28 5.1.1.Mô hình máy hữu hạn trạng thái 28 5.1.2.Ví dụ về mô hình máy hữu hạn trạng thái .28 5.2.Thực nghiệm .31 5.2.1.Áp dụng kiểm chứng mô hình hệ thống đèn .32 5.2.2.Áp dụng kiểm chứng mô hình không đáp ứng thuộc tính .33
6 Kết luận


6.1. Kết quả của khóa luận .36


6.2. Hướng nghiên cứu tiếp theo 36


Phụ lục


Phụ lục A: Tệp lampcode.txt .37





Phụ lục B: Tệp lampcode.pml khi chạy verify trong Spin .38


Phụ lục C: Tệp lamp2code.txt .40


Phụ lục D: Tệp lamp2code.pml khi chạy verify trong Spin .41


Phụ lục E: Mã nguồn của chương trình .43


Tài liệu tham khảo 47

Danh sách hình vẽ








2.1 Sơ đồ việc kiểm chứng hệ thống . 8


2.2. Sơ đồ hoạt động của phương pháp model checking 10


5.1. Mô hình máy hữu hạn trạng thái mô tả hoạt động của đèn 29


5.2. Kết quả khi chạy giả lập mô hình hệ thống đèn ở hình 5.1 .31


5.3. Kết quả kiểm chứng mô hình 5.1 của hệ thống đèn 33


5.4. Mô hình sai của hệ thống đèn .34


5.5. Kết quả kiểm chứng mô hình 5.4 của hệ thống đèn 35