LUẬN VĂN: NGHIÊN CỨU VỀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG CÔNG CỤ SPIN

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...
Nội dung trích xuất từ tài liệu:
LUẬN VĂN:NGHIÊN CỨU VỀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG CÔNG CỤ SPIN ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Trần Thị Vân DungNGHIÊ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 DungNGHIÊ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 - 2010Lờ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 trongsuố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ôngnghệ, 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 đạihọ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 DungTó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ệckiể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áivà 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 trongnhững bộ kiểm chứng (model checker) được sử dụng rộng rãi. Các bộ kiểm chứng khôngkiể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ểmchứ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àycù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ểmchứ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. 1MỤC LỤCMục Lục1 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 .......................................................................................... 72 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 .................................................... ..103 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 ........ ...