ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Trần Thị Vân Dung
NGHIÊN CỨU VỀ KIỂM CHỨNG PHẦN MỀM SỬ
DỤNG CÔNG CỤ SPIN
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công Nghệ Thông Tin
HÀ NỘI - 2010
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Trần Thị Vân Dung
NGHIÊN CỨU VỀ KIỂM CHỨNG PHẦN MỀM SỬ
DỤNG CÔNG CỤ SPIN
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công Nghệ Thông Tin
Cán bộ hướng dẫn: PGS. TS. Nguyễn Việt Hà
Cán bộ đồng hướng dẫn: TS. Phạm Ngọc Hùng
HÀ NỘI - 2010
Lời cảm ơn
Lời đầu tiên, em xin đƣợc bày tỏ lòng biết ơn sâu sắc tới thầy TS. Nguyễn Việt Hà
và thầy TS. Phạm Ngọc Hùng đã tận tình giúp đỡ em làm và hoàn thiện khóa luận trong
suốt năm học vừa qua.
Em xin đƣợc bày tỏ lòng biết ơn tới các thầy, cô trong khoa Công Nghệ Thông Tin,
trƣờng Đại Học Công Nghệ, ĐHQGHN. Các thầy cô đã nhiệt tình dạy bảo và tạo mọi
điều kiện học tập tốt nhất cho chúng em trong những năm học tập tại ĐHCN, đặc biệt là
trong thời gian thực hiện khóa luận tốt nghiệp.
Tôi xin cảm ơn các bạn sinh viên lớp K51CC và K51CNPM Trƣờng Đại học Công
nghệ, những ngƣời bạn đã cùng tôi học tập và rèn luyện trong suốt những năm học đại
học.
Cuối cùng con xin gửi tới Bố Mẹ và gia đình tình thƣơng yêu và lòng biết ơn. Bố Mẹ
đã nuôi dƣỡng và luôn là chỗ dựa tinh thần cho con.
Hà Nội, ngày 18 tháng 5 năm 2010
Trần Thị Vân Dung
1
Tóm tắt nội dung
Kiểm chứng mô hình (model checking) là một phƣơng pháp hình thức dùng cho việc
kiểm chứng hệ thống. Kiểm chứng mô hình khảo sát tất cả các trạng thái có thể của hệ
thống và kiểm tra rằng chúng chứa sự đúng đắn đã đƣợc đặc tả. Việc sinh ra các trạng thái
và kiểm tra có thể đƣợc thực hiện một cách tự động bằng phần mềm và Spin là một trong
những bộ kiểm chứng (model checker) đƣợc sử dụng rộng rãi. Các bộ kiểm chứng không
kiểm tra trực tiếp chƣơng trình mà kiểm tra một mô hình là thể hiện mức cao của hệ
thống. Mô hình này mô tả hành vi của hệ thống. Để áp dụng đƣợc các công cụ kiểm
chứng mô hình, việc đầu tiên là phải xây dựng mô hình của hệ thống. Các mô hình này
cùng với đặc tả của thuộc tính cần kiểm tra là đầu vào của các bộ kiểm chứng.
Khóa luận nghiên cứu việc kiểm chứng phần mềm sử dụng Spin, cụ thể là việc kiểm
chứng mô hình máy hữu hạn trạng thái, sau đó đƣa ra một công cụ chuyển một mô tả ban
đầu của hệ thống ở dạng máy hữu hạn trạng thái (chứa trong 1 tệp .txt) thành mô hình và
kiểm chứng bằng Spin.
MỤC LỤC
2
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