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.

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

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

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

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ế . 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ế .

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 . 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:

Hình 2.1. Nguyên tắc họat động của kiểm chứng mô hình .

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

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.