LUẬN VĂN: KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV

Kiểm chứng mô hình (model checking) là một hướng tiếp cận hiệu quả cho việc đảm bảo chất lượng phần mềm. Kĩ thuật này được áp dụng để chứng minh một cách tự động tính đúng đắn của phần mềm hoặc chỉ ra tại sao phần mềm không chạy đúng thông qua phản ví dụ.Hiện nay có rất nhiều công cụ kiểm chứng mô hình phần mềm như NuSMV, SPIN, KRONOS ...
Nội dung trích xuất từ tài liệu:
LUẬN VĂN:KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nông Gia Tự KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV 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Ệ Nông Gia Tự KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV 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: TS. Phạm Ngọc Hùng HÀ NỘI - 2010 Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự Lời cảm ơn Lời đầu tiên em xin bày tỏ lòng biết ơn sâu sắc tới TS. Phạm Ngọc Hùng, thầy đã hướng dẫn em tận tình trong suốt năm học vừa qua. Em xin bày tỏ lòng biết ơn tới các thầy, cô giáo trong Khoa Công nghệ thông tin - Trường Đại học Công nghệ - ĐHQGHN. Các thầy cô đã dạy bảo, chỉ dẫn chúng em và luôn tạo điều kiện tốt nhất cho chúng em học tập trong suốt quá trình học đại học đặc biệt là trong thời gian làm khoá luận tốt nghiệp. Tôi xin cảm ơn các bạn sinh viên lớp K51CD và lớp K51CNPM đã cho tôi những ý kiến đóng góp giá trị cùng những lời động viên khích lệ khi thực hiện đề tài này. Cuối cùng con xin gửi tới bố mẹ và toàn thể gia đình lòng biết ơn và tình cảm yêu thương. Hà Nội, ngày 15 tháng 5 năm 2008 Nông Gia Tự i Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự Tóm tắt Kiểm chứng mô hình (model checking) là một hướng tiếp cận hiệu quả cho việc đảm bảo chất lượng phần mềm. Kĩ thuật này được áp dụng để chứng minh một cách tự động tính đúng đắn của phần mềm hoặc chỉ ra tại sao phần mềm không chạy đúng thông qua phản ví dụ. Hiện nay có rất nhiều công cụ kiểm chứng mô hình phần mềm như NuSMV, SPIN, KRONOS ... Khóa luận này nghiên cứu lý thuyết cơ bản vè kiểm chứng mô hình, ngôn ngữ SMV dùng để mô hình hóa hệ thống và cách sử dụng NuSMV để kiểm chứng mô hình phần mềm. Kiểm chứng mô hình thường được áp dụng ở giai đoạn thiết kế vì việc mô hình hóa bản thiết kế hệ thống dễ dàng hơn mô hình hóa mã nguồn của hệ thống. Ngoài ra, việc sớm tìm ra lỗi ở bản thiết kế sẽ giúp giảm thiểu rủi ro của quá trình phát triển phần mềm. Vì thế chúng tôi tập trung tìm hiểu và đề xuất quy trình kiểm chứng mô hình sử dụng NuSMV ở giai đoạn thiết kế phần mềm. Đồng thời áp dụng quy trình này để kiểm chứng mô hình của phần mềm giả lập máy rút tiền tự động ATM. ii Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự Mục lục Chương 1 Giới thiệu ........................................................................................1 1.1 Đặt vấn đề.........................................................................................1 1.2 Nội dung nghiên cứu của khóa luận ..................................................2 1.3 Cấu trúc khóa luận ............................................................................2 Chương 2 Tổng quan về kiểm chứng mô hình và NuSMV ..............................4 2.1 Tổng quan về kiểm chứng mô hình ...................................................4 2.1.1 Giới thiệu ......................................................................................4 2.1.2 Ý nghĩa của kiểm chứng mô hình ..................................................5 2.1.3 Sự khác nhau giữa kiểm chứng mô hình phần mềm và kiểm thử phần mềm 5 2.2 NuSMV ............................................................................................6 2.2.1 Giới thiệu ......................................................................................6 2.2.2 Kiến trúc của NuSMV ...................................................................6 2.2.3 Sử dụng NuSMV để kiểm chứng mô hình .....................................8 Chương 3 Giới thiệu về logic thời gian ............................................................9 3.1 Khái niệm .........................................................................................9 3.2 Các toán tử trong logic thời gian .......................................................9 3.2.1 Toán tử globally (toàn thể) ............................................................9 3.2.2 Toán tử next (tiếp theo) ............................................................... 10 3.2.3 Toán tử eventually (cuối cùng sẽ xảy ra) .....................................10 3.3 TLT và CTL ................................................................................... 10 3.4 Sử dụng temporal logic để mô tả một số thuộc tính cần kiểm chứng 11 3.4.1 Safety (tính an toàn) ....................................................................11 3.4.2 Liveness (tính chạy được) ........................................................... 11 3.4.3 Fairness (tính công bằng) ............................................................ 12 Chương 4 Ngôn ngữ SMV............................................................................. 13 4.1 Tổng quan ....................................................................................... 13 4.2 Cấu trúc của chương trình viết bằng ngôn ngữ SMV ....................... 13 4.3 Các kiểu dữ liệu .............................................................................. 13 4.3.1 Khai báo kiểu dữ liệu ..................................................................13 iii Kiểm chứng mô h ...