- 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. - 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. - 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.. - 4Chương 2 Tổng quan về kiểm chứng mô hình và NuSMV. - Tổng quan về kiểm chứng mô hình. - Ý nghĩa của kiểm chứng mô hình. - 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. - Sử dụng NuSMV để kiểm chứng mô hình. - 20Áp dụng NuSMV kiểm chứng mô hình phần mềm giả lập máy ATM. - Đặc tả và kiểm chứng mô hình phần mềm giả lập máy ATM. - 225.2.1.3 Mô hình ca sử dụng tổng thể hệ thống. - Đặc tả các thuộc tính cần kiểm chứng. - Mô hình hóa hệ thống bằng ngôn ngữ SMV. - 285.2.4.1 Mô hình hóa tổng thể hệ thống. - 295.2.4.2 Mô hình hóa quá trình thực hiện phiên làm việc. - 315.2.4.3 Mô hình hóa quá trình thực hiện giao dịch. - Kiểm chứng mô hình. - Nguyên tắc họat động của kiểm chứng mô hình.. - Mô hình tổng thể hệ thống viết bằng ngôn ngữ SMV.. - 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.. - 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.. - Kết quả kiểm chứng mô hình tổng thể hệ thống. - Kết quả kiểm chứng mô hình phiên làm việc của hệ thống. - 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 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. - 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.. - 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.. - 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 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.. - 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. - 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. - 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. - 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. - 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. - 2.1.2 Ý nghĩa của kiểm chứng mô hình. - 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. - 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. - 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. - 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]. - 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. - 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. - 2.2.3 Sử dụng NuSMV để kiểm chứng mô hình. - Để kiểm chứng mô hình bằng NuSMV, chúng ta cần mô tả hệ thống và đặc tả các thuộc tính bằng ngôn ngữ SMV. - Ngôn ngữ SMV có thể dùng để thiết lập mô hình dùng cho việc kiểm chứng.. - Áp dụng NuSMV kiểm chứng mô hình phần mềm giả lập máy ATM. - 4.7.1 Những cơ sở để đưa ra quy trình Để kiểm chứng một mô hình cần phải thực hiện hai bước: đầu tiên phải mô hình hóa phần mềm cần kiểm chứng sau đó cần định nghĩa các thuộc tính cần kiểm chứng. - Đối với trường hợp sử dụng NuSMV thì chúng ta cần hai bước là mô hình hóa bằng ngôn ngữ SMV và khai báo các thuộc tính cần kiểm chứng bằng temporal logic. - Việc xây dựng mô hình có ý nghĩa vô cùng quan trọng. - Nếu mô hình được xây dựng không chính xác, nó sẽ không mô tả đúng hệ thống cần kiểm chứng. - Ngoài ra, do việc xây dựng mô hình bằng ngôn ngữ SMV được thực hiện thủ công nên có thể xảy ra sai sót. - Dựa vào tính chất này, chúng ta sẽ tìm cách xây dựng các biểu đồ trạng thái của hệ thống cần kiểm chứng rồi từ biểu đồ trạng thái xây dựng mô hình bằng ngôn ngữ SMV.. - Đối tượng của kiểm chứng chính là mô hình hoạt động dự kiến của phần mềm. - Bước 3: Từ biểu đồ trạng thái chúng ta xây dựng mô hình bằng ngôn ngữ SMV. - Đưa các đặc tả thuộc tính này vào file mô hình hóa bằng ngôn ngữ SMV.. - Bước 4: Sử dụng NuSMV để kiểm chứng mô hình có thỏa mãn các thuộc tính đã đặc tả hay không.. - 4.8 Đặc tả và kiểm chứng mô hình phần mềm giả lập máy ATM. - Đối tượng của kiểm chứng chính là mô hình hoạt động dự kiến của phần mềm.. - 4.8.1.3 Mô hình ca sử dụng tổng thể hệ thống. - Tuy nhiên, do trong quy trình kiểm chứng phần mềm chúng ta xây dựng mô hình dựa trên biểu đồ trạng thái nên ở đây, để cho ngắn gọn, chúng ta chỉ xét đến một số biểu đồ trạng thái nhằm minh họa cho việc thực hiện quy trình. - 4.8.4 Mô hình hóa hệ thống bằng ngôn ngữ SMV 4.8.4.1 Mô hình hóa tổng thể hệ thống. - Dựa vào biểu đồ trạng thái tổng thể hệ thống, chúng ta xây dựng được mô hình bằng ngôn ngữ SMV như sau: MODULE main VAR state_overall: {TAT, CHO, PHUC_VU}. - Mô hình tổng thể hệ thống viết bằng ngôn ngữ SMV. - Trong mô hình này, chúng ta cần đảm bảo rằng hệ thống từ trạng thái đang ngừng họat động đến một lúc nào đó có thể đến trạng thái phục vụ người dùng (liveness). - 4.8.4.2 Mô hình hóa quá trình thực hiện phiên làm việc Dựa vào biểu đồ trạng thái quá trình thực hiện phiên làm việc của hệ thống (hình 5.3), chúng ta xây dựng được mô hình bằng ngôn ngữ SMV như sau: MODULE main VAR state_session: {DOC_THE,. - 4.8.4.3 Mô hình hóa quá trình thực hiện giao dịch Dựa vào biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống (hình 5.4), chúng ta xây dựng được mô hình bằng ngôn ngữ SMV như sau: MODULE main VAR state_transaction: {LAY_THONG_TIN,. - 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. - 4.8.5 Kiểm chứng mô hình Kết quả kiểm chứng cho thấy mô hình được thiết kế hoàn toàn thỏa mãn các thuộc tính đặt ra:. - Kết quả kiểm chứng mô hình tổng thể hệ thống.. - Kết quả kiểm chứng mô hình phiên làm việc của hệ thống.. - Kết quả kiểm chứng mô hình thực hiện giao dịch hệ thống. - Trong khóa luận này chúng tôi đã trình bày những lý thuyết cơ bản về kiểm chứng mô hình phần mềm, nghiên cứu và áp dụng kỹ thuật kiểm chứng mô hình sử dụng NuSMV như là một công cụ kiểm chứng.. - Chúng tôi đã đề xuất quy trình kiểm chứng mô hình phần mềm ở giai đoạn thiết kế hệ thống sử dụng NuSMV. - Quy trình này được áp dụng 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 và đã chứng minh được bản thiết kế hoàn toàn thỏa mãn các thuộc tính đặt ra. - Khóa luận đã áp dụng thành công kỹ thuật kiểm chứng mô hình vào kiểm chứng ở giai đoạn thiết kế phần mềm. - Tuy nhiên, chúng tôi chưa xét đến việc thẩm định lại bản thiết kế hệ thống nếu công cụ kiểm chứng trả về kết quả mô hình hệ thống không thỏa mãn các thuộc tính. - Khi đó có thể do bản thiết kế hệ thống sai hoặc bị mô hình hóa sai. - Một hướng khác là xây dựng công cụ mô hình hóa tự động bản thiết kế phần mềm.. - KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV