Đề tài 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ự i 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ự Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự ii 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. Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự iii 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 Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự iv 4.3.2 Kiểu logic (boolean), kiểu số nguyên (integer) và kiểu liệt kê (enum) 14 4.3.3 Mảng...........................................................................................14 4.3.4 Mảng nhiều chiều ........................................................................15 4.3.5 Kiểu cấu trúc ...............................................................................15 4.4 Biến và các phép gán ......................................................................16 4.5 Các phép toán .................................................................................16 4.5.1 Phép gán .....................................................................................16 4.5.2 Tóan tử next ................................................................................17 4.6 Máy trạng thái.................................................................................18 Chương 5 ......................................................................................................20 Áp dụng NuSMV kiểm chứng mô hình phần mềm giả lập máy ATM............20 5.1 Đề xuất quy trình đặc tả và kiểm chứng phần mềm sử dụng NuSMV 20 5.1.1 Những cơ sở để đưa ra quy trình .................................................20 5.1.2 Mô tả quy trình............................................................................21 5.2 Đặc tả và kiểm chứng mô hình phần mềm giả lập máy ATM ..........21 5.2.1 Đặc tả yêu cầu.............................................................................21 5.2.1.1 Mô tả bài toán.............................................................................21 5.2.1.2 Các tác nhân của hệ thống ..........................................................22 5.2.1.3 Mô hình ca sử dụng tổng thể hệ thống ........................................22 5.2.1.4 Bật máy ......................................................................................23 5.2.1.5 Tắt máy ......................................................................................23 5.2.1.6 Phiên làm việc ............................................................................24 5.2.1.7 Giao dịch rút tiền ........................................................................24 5.2.1.8 Giao dịch chuyển tiền .................................................................24 5.2.1.9 Giao dịch vấn tin tài khoản .........................................................25 5.2.1.10 Sai mã PIN ...............................................................................25 5.2.2 Đặc tả các thuộc tính cần kiểm chứng .........................................25 5.2.3 Thiết kế hệ thống ........................................................................25 5.2.3.1 Biểu đồ trạng thái tổng thể hệ thống ...........................................25 5.2.3.2 Biểu đồ trạng thái quá trình thực hiện một phiên làm việc của hệ thống ..............................................................................................................26 5.2.3.3 Biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống .....27 Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự v 5.2.4 Mô hình hóa hệ thống bằng ngôn ngữ SMV ................................28 5.2.4.1 Mô hình hóa tổng thể hệ thống ...................................................28 5.2.4.2 Mô hình hóa quá trình thực hiện phiên làm việc .........................29 5.2.4.3 Mô hình hóa quá trình thực hiện giao dịch ..................................31 5.2.5 Kiểm chứng mô hình...................................................................33 Chương 6 Kết luận ........................................................................................35 Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự vi Danh mục hình vẽ Hình 2.1. Nguyên tắc họat động của kiểm chứng mô hình. Hình 2.2. Sơ đồ kiến trúc NuSMV. Hình 5.1. Biểu đồ ca sử dụng hệ thống máy ATM. Hình 5.3. Biểu đồ trạng thái quá trình thực hiện một phiên làm việc của hệ thống ATM. Hình 5.4. Biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống ATM. Hình 5.5. Mô hình tổng thể hệ thống viết bằng ngôn ngữ SMV. Hình 5.6. Mô hình quá trình thực hiện một phiên làm việc của hệ thống bằng ngôn ngữ SMV. Hình 5.7. Mô hình quá trình thực hiện giao dịch của hệ thống ATM bằng ngôn ngữ SMV. Hình 5.8. Kết quả kiểm chứng mô hình tổng thể hệ thống. Hình 5.9. Kết quả kiểm chứng mô hình phiên làm việc của hệ thống. Hình 5.10. Kết quả kiểm chứng mô hình thực hiện giao dịch hệ thống. Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự vii Danh mục từ viết tắt Ký hiệu Thuật ngữ ATM Automated Teller Machine BDD Binary Decision Diagram CTL Computation Tree Logic LTL Linear Time Logic Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự 1 Chương 1 Giới thiệu 1.1 Đặt vấn đề Việc đảm bảo chất lượng phần mềm là một trong những công đoạn khó khăn nhất của việc phát triển phần mềm. Trong đó, việc đảm bảo tính đúng đắn của bản thiết kế ở bước sớm nhất có thể là một thách thức lớn nhất đối với bất kì quy trình phát triển phần mềm nào. Từ trước đến nay, phương pháp giả lập và kiểm thử thường được sử dụng để kiểm tra các bản thiết kế [5]. Tuy nhiên phương pháp này bộc lộ nhiều khiếm khuyết trong đó điểm yếu nghiêm trọng nhất chính là không thể khẳng định được chương trình đã hết lỗi hoặc ước lượng được số lỗi có thể sót lại trong bản thiết kế [5]. Kiểm chứng mô hình là một kỹ thuật kiểm chứng tự động các hệ thống hữu hạn trạng thái. Kiểm chứng mô hình xác minh tính đúng đắn của một mô hình bằng việc xác định xem các thuộc tính người dùng mong muốn có được thỏa mãn bởi mô hình đó hay không [6]. Về nguyên tắc hoạt động, hệ thống cần kiểm chứng sẽ được mô hình hóa. Công cụ kiểm chứng sẽ kiểm tra mô hình có thỏa mãn các thuộc tính được cho hay không. Nhờ khả năng duyệt qua tất cả các trạng thái trong mô hình mà tính đúng đắn của kết quả kiểm chứng mô hình luôn được đảm bảo. Nguyên tắc họat động của kiểm chứng mô hình như sau: Đóng vai trò xử lý dữ liệu tự động là một công cụ kiểm chứng mô hình. Đầu vào là hệ thống cần kiểm chứng đã được mô hình hóa và mô tả các thuộc tính cần kiểm chứng. Đầu ra là kết quả kiểm chứng – kết luận hệ thống hoàn toàn thỏa mãn các thuộc tính hoặc kết luận hệ thống không thỏa mãn một hoặc nhiều thuộc tính đi kèm với phản ví dụ. Nguyên tắc này được minh họa trong hình sau: Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự 2 Hình 2.1. Nguyên tắc họat động của kiểm chứng mô hình [7]. Trong quá trình kiểm chứng mô hình, việc mô hình hóa hệ thống và đặc tả các thuộc tính thường được thực hiện thủ công. Việc chứng minh mô hình có thỏa mãn các thuộc tính hay không đựơc thực hiện tự động bằng công cụ kiểm chứng mô hình. Khóa luận này tập trung nghiên cứu và áp dụng công cụ kiểm chứng mô hình NuSMV vào việc kiểm chứng ở giai đoạn thiết kế phần mềm. 1.2 Nội dung nghiên cứu của khóa luận NuSMV là một công cụ kiểm chứng mô hình mã nguồn mở. Đầu vào của NuSMV là một file viết bằng ngôn ngữ SMV trong đó mô tả mô hình hệ thống và các đặc tả thuộc tính cần kiểm chứng. Khóa luận nghiên cứu lý thuyết kiểm chứng mô hình và áp dụng NuSMV để kiểm chứng bản thiết kế phần mềm. Quá trình thực hiện bao gồm xác định rõ và đặc tả các thuộc tính cần kiểm chứng, mô hình hóa hệ thống và sử dụng NuSMV để phân tích, chứng minh hệ thống có thỏa mãn các thuộc tính cần kiểm chứng đó hay không. 1.3 Cấu trúc khóa luận Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự 3 Các phần còn lại của khóa luận có cấu trúc như sau: Chương 2 trình bày kiến thức cơ bản về kiểm chứng mô hình và giới thiệu về NuSMV, một công cụ kiểm chứng phần mềm. Chương 3 giới thiệu về logic thời gian và sử dụng logic thời gian để mô tả các thuộc tính cần kiểm chứng. Chương 4 trình bày về cú pháp, các kiểu dữ liệu của ngôn ngữ SMV, cách sử dụng ngôn ngữ SMV để mô tả một máy hữu hạn trạng thái. Chương 5 tìm hiểu và đề xuất quy trình kiểm chứng mô hình ở giai đoạn thiết kế phần mềm sử dụng NuSMV, sau đó áp dụng quy trình này vào kiểm chứng mô hình phần mềm giả lập máy rút tiền tự động ATM. Chương 6 nêu ra những kết luận sau khi thực hiện đề tài khóa luận và định hướng khóa luận trong tương lai. Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự 4 Chương 2 Tổng quan về kiểm chứng mô hình và NuSMV 2.1 Tổng quan về kiểm chứng mô hình 2.1.1 Giới thiệu Kiểm chứng mô hình là kỹ thuật phân tích hệ thống để xác định tính hợp lệ của một hay nhiều tính chất mà người dùng quan tâm trong một mô hình cho trước. Cụ thể hơn, với mô hình M và thuộc tính p cho trước, nó kiểm tra liệu thuộc tính p có thỏa mãn trong mô hình M hay không: M |= p [2]. Về mặt thực thi, kiểm chứng mô hình là kỹ thuật tĩnh, nó duyệt qua tất cả các trạng thái, các đường thực thi có thể có trong mô hình M để xác định tính khả thỏa của p. Trên thực tế, mô hình kiểm chứng đã chứng minh rằng nó là một phương thức hiệu quả để phát hiện nhiều lỗi trong các pha thiết kế ban đầu. Kiểm chứng mô hình bao gồm 3 bước: Mô hình hóa, đặc tả và kiểm chứng. Ở bước mô hình hóa, kết quả tạo ra là một mô hình mà các công cụ kiểm chứng có thể sử dụng được. Đầu vào của bước này có thể là bản thiết kế phần mềm hoặc là các dòng mã lập trình. Trong bước tiếp theo, các thuộc tính mà bản thiết kế cần thỏa mãn được đặc tả. Các thuộc tính này thường được diễn đạt bằng các biểu thức logic. Kết quả của hai bước mô hình hóa và đặc tả chính là đầu vào của kiểm chứng mô hình. Ở bước cuối cùng, kiểm chứng, công cụ kiểm chứng sẽ tự động thực hiện và trả về kết quả là thỏa mãn nếu mô hình thỏa mãn các thuộc tính, hoặc đưa ra một phản ví dụ nếu mô hình không thỏa mãn. Dựa vào phản ví dụ, người ta có thể tìm ra được lý do vì sao mô hình không thỏa mãn các thuộc tính đặt ra. Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự 5 Tóm lại, kiểm chứng mô hình là một kĩ thuật giúp kiểm tra một chương trình hoặc một bản thiết kế có thỏa mãn các tính chất đặt ra hay không một cách tự động. Đầu vào của nó là một mô hình cần kiểm chứng và các thuộc tính mà nó cần thỏa mãn. Đầu ra là kết luận mộ hình thỏa mãn các tính chất hoặc đưa ra một phản ví dụ nếu mô hình không thỏa mãn. 2.1.2 Ý nghĩa của kiểm chứng mô hình Các hệ thống phần mềm đang ngày càng trở nên cần thiết và đóng vai trò quan trọng trong đời sống hàng ngày. Nhiều công việc có mức độ ảnh hưởng lớn được thực hiện bởi phần mềm như điều khiển đèn giao thông, giao dịch ngân hàng, điều khiển các thiết bị y tế ... Những phần mềm thực hiện các công việc đó phải đảm bảo có độ tin cậy rất cao và không được phép xuất hiện lỗi. Kiểm chứng mô hình cho phép khẳng định được phần mềm hoàn toàn không còn lỗi và thực hiện được đúng các chức năng đã đặt ra. Ngòai ra, kiểm chứng phần mềm còn có ý nghĩa quan trọng trong quy trình phát triển phần mềm. Nó cho phép tìm ra được các lỗi ngay từ giai đoạn thiết kế của quy trình phát triển. Điều này có vai trò rất quan trọng vì các lỗi từ giai đoạn thiết kế nếu tìm ra muộn có thể gây thiệt hại rất lớn so với các lỗi của giai đoạn sau. 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 Cả kiểm chứng mô hình và kiểm thử phần mềm đều thực hiện vai trò đảm bảo chất lượng phần mềm bằng việc tìm ra các lỗi nếu có của phần mềm. Tuy nhiên giữa kiểm chứng mô hình và kiểm thử phần mềm có một số điểm khác nhau quan trọng sau: Kiểm thử phần mềm đòi hỏi phải có chương trình để thực hiện, còn kiểm chứng mô hình thì ngoài kiểm thử trên mã nguồn còn có thể dùng để kiểm chứng bản thiết kế, nghĩa là khi chương trình vẫn còn trên giấy. Kiểm thử phần mềm chỉ có thể khẳng định được chương trình không gặp lỗi đối với các trường hợp kiểm thử đã kiểm tra tức không tìm thấy lỗi chứ không khẳng định được là chương trình hoàn toàn không còn lỗi. Ngược lại, kiểm chứng phần mềm cho phép ta kết luận được chương trình hoàn toàn không còn lỗi. Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự 6 Tuy nhiên, kiểm thử phần mềm có ưu điểm rất lớn là dễ thực hiện. Một người bình thường cũng có thể thực hiện được. Trong khi đó, kiểm chứng mô hình đòi hỏi phải mô hình hóa và đặc tả, công việc này rất khó và đòi hỏi người thực hiện có trình độ kinh nghiệm và kiến thức nhất định. Tóm lại, kiểm chứng mô hình là một phương pháp hiệu quả nhất để kiểm chứng phần mềm. Tuy nhiên để sử dụng được nó một cách hiệu quả đòi hỏi phải mất nhiều thời gian và công sức để nghiên cứu và thực hiện. 2.2 NuSMV 2.2.1 Giới thiệu NuSMV là một công cụ kiểm chứng mô hình được trường đại học Carnegie Mellon University (CMU) và viện per la Ricerca Scientifica e Tecnolgica (IRST). NuSMV được thiết kế với kiến trúc mở, mềm dẻo và được mô tả đầy đủ để phục vụ cho việc kiểm chứng mô hình phần mềm [4]. NuSMV có thể xử lý file viết bằng ngôn ngữ SMV. File này chứa hệ thống đã được mô hình hóa và các đặc tả thuộc tính mà hệ thống cần kiểm chứng. Sau khi xử lý, NuSMV sẽ đưa ra thông báo hệ thống có thỏa mãn các thuộc tính đó hay không, nếu hệ thống không thỏa mãn, NuSMV sẽ đưa ra phản ví dụ. NuSMV hỗ trợ cả đặc tả thuộc tính bằng LTL và CTL. 2.2.2 Kiến trúc của NuSMV NuSMV có kiến trúc mở, dễ dàng chỉnh sửa, mở rộng hay nâng cấp. Kiến trúc của NuSMV được chia thành các module. Mỗi module đảm trách một tập hợp các chức năng và giao tiếp với các module khác qua những giao diện đã được định nghĩa rõ ràng. Phần lõi và phần ngoại vi của kiến trúc được tách biệt rõ ràng nhằm giúp cho các module bên trong có thể sử dụng lại một cách độc lập với ngôn ngữ dùng để mô hình hóa hệ thống. Kiến trúc của NuSMV (hình 4.1) bao gồm các module sau:  Kernel: Phần lõi. Module này cung cấp các chức năng ở mức độ thấp như cấp phát bộ nhớ động, tổ chức các cấu trúc dữ liệu. Module này có thể Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự 7 được sử dụng lại như những hộp đen (black-box) với những hàm đã được mô tả rõ ràng.  Parser: Bộ phân tích ngữ pháp. Module này xử lý file viết bằng ngôn ngữ SMV, kiểm tra về mặt cú pháp và xây dựng cấu trúc cây biểu diễn cấu trúc bên trong của file được xử lý.  Compiler: Chương trình dịch. Module này có chức năng dịch file SMV sau khi đã phân tích ngữ pháp sang cây quyết định nhị phân (binary decision diagram - BDD). Mô hình hệ thống được chuyển thành máy hữu hạn trạng thái nhờ module này.  Model Checking: Bộ kiểm chứng mô hình. Module này kiểm tra các thuộc tính được mô tả bằng CTL và sinh ra các phản ví dụ nếu thuộc tính không được thỏa mãn bởi mô hình.  LTL: Module này có