ĐẠ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.

Chương 2
Tổng quan về kiểm chứng mô hình và NuSMV...........................................................4
1.4Tổng quan về kiểm chứng mô hình.............................................................4
1.4.1Giới thiệu..............................................................................................4
1.4.2Ý nghĩa của kiểm chứng mô hình.........................................................5
1.4.3Sự 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
1.5NuSMV........................................................................................................6
1.5.1Giới thiệu..............................................................................................6
1.5.2Kiến trúc của NuSMV..........................................................................6
1.5.3Sử dụng NuSMV để kiểm chứng mô hình............................................8
Chương 3
Giới thiệu về logic thời gian..........................................................................................9
1.6Khái niệm.....................................................................................................9
1.7Các toán tử trong logic thời gian.................................................................9
1.7.1Toán tử globally (toàn thể)....................................................................9
1.7.2Toán tử next (tiếp theo).......................................................................10
1.7.3Toán tử eventually (cuối cùng sẽ xảy ra) ...........................................10
1.8TLT và CTL...............................................................................................10
1.9Sử dụng temporal logic để mô tả một số thuộc tính cần kiểm chứng........10
1.9.1Safety (tính an toàn)............................................................................11
1.9.2Liveness (tính chạy được)...................................................................11
1.9.3Fairness (tính công bằng)....................................................................12
Chương 4
Ngôn ngữ SMV...........................................................................................................13
1.10Tổng quan................................................................................................13
1.11Cấu trúc của chương trình viết bằng ngôn ngữ SMV..............................13
iii
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
1.12Các kiểu dữ liệu.......................................................................................13

1.17.3.2Biể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
1.17.3.3Biểu đồ trạng thái quá trình thực hiện giao dịch của hệ thống......27
iv
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
....................................................................................................................28
1.17.4Mô hình hóa hệ thống bằng ngôn ngữ SMV.....................................28
1.17.4.1Mô hình hóa tổng thể hệ thống......................................................28
1.17.4.2Mô hình hóa quá trình thực hiện phiên làm việc............................29
1.17.4.3Mô hình hóa quá trình thực hiện giao dịch....................................31
1.17.5Kiểm chứng mô hình.........................................................................33
Chương 6
Kết luận.......................................................................................................................35
v
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
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.

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:
1
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
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
Các phần còn lại của khóa luận có cấu trúc như sau:
2
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
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.

do vì sao mô hình không thỏa mãn các thuộc tính đặt ra.
4
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
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.
1.4.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.
1.4.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

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ể được
6
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
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ó chức năng dịch các biểu thức LTL thành các hoạt cảnh
(tableaux) thích hợp để NuSMV có thể xử lý được.
• Interactive shell: Giao diện tương tác dòng lệnh. Module này cung cấp giao
diện người dùng ở chế độ dòng lệnh.
• Graphical user interface: Giao diện đồ họa người dùng. Module này được
xây dựng bên trên module giao diện tương tác dòng lệnh nhằm cung cấp một
giao diện đồ họa trực quan của chương trình cho người sử dụng.
Hình 2.2. Sơ đồ kiến trúc NuSMV [4].
7
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự
1.5.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. Sau đó sử dụng lệnh: