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

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

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

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.

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

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

Trong các nghiên cứu về kiểm chứng mô hình, hai loại logic thời gian hay
được xem xét là LTL và CTL [1].
3.2 Các toán tử trong logic thời gian
3.2.1 Toán tử globally (toàn thể)
Toán tử globally kí hiệu là □. Giả sử ϕ là một biểu thức logic vị từ, khi đó biểu
thức □ϕ có giá trị đúng nếu ϕ đúng trong mọi thời điểm. Người ta cũng thường kí
hiệu toán tử này là G.
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự

10
3.2.2 Toán tử next (tiếp theo)
Toán tử next kí hiệu là ○. Giả sử ϕ là một biểu thức logic. Có thể coi ϕ như
một dãy trạng thái và trạng thái hiện tại đang xét đến là trạng thái thứ n. Khi đó biểu
thức ○ϕ có giá trị đúng khi và chỉ khi phần tử ngay sau phần tử hiện tại trong dãy
trạng thái ϕ (phần tử thứ n+1) có giá trị đúng. (bằng 1)
Toán tử next thường được kí hiệu bằng chữ cái X.
3.2.3 Toán tử eventually (cuối cùng sẽ xảy ra)
Toán tử eventually kí hiệu là ◊. Giả sử ϕ là một biểu thức logic và ϕ được coi
như một dãy trạng thái mà mỗi phần tử chỉ có giá trị bằng 0 hoặc 1. Khi đó giá trị
biểu thức ◊ϕ bằng 1 khi và chỉ khi ϕ có ít nhất một phần tử có giá trị bằng 1. Toán
tử ◊ được định nghĩa thông qua toán tử □ như sau:
◊ϕ ≡ □ φ
Toán tử eventually thường được kí hiệu bằng chữ cái F.
3.3 TLT và CTL
Các biểu thức temporal logic không chỉ xét đến những dãy trạng thái đơn, mà
còn xét đến những dãy trạng thái phức tạp trong đó từ một trạng thái có thể có nhiều
trạng thái ngay tiếp sau nó. Trong các nghiên cứu về kiểm chứng mô hình, hai loại
logic thời gian hay được xem xét là LTL và CTL:
 LTL (linear-time-temporal logic): Logic thời gian tuyến tính. Thời gian
có cấu trúc tuyến tính, mỗi trạng thái chỉ có một trạng thái ngay tiếp sau

AF done
AG (req → AF grant)
AG AF tick
trong CTL hoặc
F done
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự

12
G (req → F grant)
G F tick
trong LTL.
Ví dụ:
 Khi chìa khóa xe vặn tới vị trí khởi động, xe sẽ nổ máy.
 Bóng đèn sẽ chuyển sang màu xanh
3.4.3 Fairness (tính công bằng)
Tính công bằng đảm bảo rằng nếu một sự kiện nào đó ở trạng thái sẵn sàng
được thực thi thì đến một lúc nào đó nó sẽ được thực thi.
Thuộc tính công bằng có thể được biểu diễn bằng các toán tử AF và phép suy
ra:
AG (san_sang=0 → AF thuc_thi=0)
AG (san_sang=1→ AF thuc_thi =1)
Một ví dụ cho tính công bằng trong một hệ thống truyền-nhận tin là khi một
gói tin được gửi đi thì đến một lúc nào đó nó sẽ đến được đích.
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự

13

Chương 4
Ngôn ngữ SMV
4.1 Tổng quan

thì biến var1 chỉ có thể có giá trị bằng 1 hoặc 0.
Kiểu liệt kê là một tập hợp các giá trị. Ví dụ, câu lệnh
var1: {ready, willing, able};
khai báo một biến có thể có các giá trị là ‘ready’, ‘willing’, ‘able’. Ngoài ra,
các giá trị của một kiểu biến liệt kê có thể là các số nguyên. Ví dụ như câu lệnh sau
khai báo một biến có tên là count có thể có các giá trị là những số nguyên từ 0 đến
7:
count: 0 7;
Các giá trị số trong khai báo biến cũng có thể là các biểu thức chứa các chữ số
và các toán tử như +, - , *, /, mod, <<, >> và **.
4.3.3 Mảng
Một mảng trong ngôn ngữ SMV được khai báo theo dạng sau:
<tên_biến> : array <x> <y> of <kiểu giá trị>
Câu lệnh trên sẽ khai báo một mảng các phần tử có kiểu là <kiểu giá trị>, chỉ
số của phần tử chạy từ <x> đến <y>. Ví dụ, câu lệnh:
var1 : array 2 0 of boolean;
tương đương với khai báo như sau:
var1[2] : boolean;
var1[1] : boolean;
var1[0] : boolean;
Một phần tử của mảng có thể được tham chiếu nhờ chỉ số của nó nằm trong
dấu ngoặc vuông viết sau tên biến. Nhưng chỉ số này cần phải nằm trong khoảng đã
khai báo.
Kiểm chứng mô hình phần mềm sử dụng NuSMV Nông Gia Tự

15
4.3.4 Mảng nhiều chiều
Một mảng trong ngôn ngữ SMV được khai báo theo dạng sau:
Một mảng hai chiều có thể được coi như một mảng của mảng. Ví dụ, câu lệnh:
matrix : array 0 1 of array 2 0 of boolean;

16

foo.cn : kiểu_n;
Như vậy, kiểu cấu trúc cũng giống như kiểu mảng ở điểm có thể chứa nhiều
phần tử với những kiểu dữ liệu khác nhau
4.4 Biến và các phép gán
Giá trị của một biến là một chuỗi các giá trị. Chuỗi này không giới hạn về độ
dài và các giá trị của chuỗi phải thuộc kiểu dữ liệu của biến đó. Ví dụ, một biến kiểu
logic có thể có giá trị bằng:
0;1;0;1;
4.5 Các phép toán
Như ta đã biết, giá trị của một biến có thể là một chuỗi các phần tử. Một phép
toán tác động đến từng phần tử đó. Ví dụ, xét trường hợp phép toán NOT, ký hiệu là
“~”, áp dụng cho biến sau:
foo = 0;1;0;1;
ta được kết quả
~foo = 1;0;1;0;
Một phép toán khác là phép toán AND, ký hiệu là “&”. Ví dụ:
foo = 0;1;0;1;
và
bar = 0;0;1;1;
khi đó
foo & bar = 0;0;0;1;
4.5.1 Phép gán
Như ta đã biết, giá trị của một biến có thể là một chuỗi các phần tử. Một phép
toán tác động đến từng phần tử đó. Ví dụ, xét trường hợp phép toán NOT, ký hiệu là
“~”, áp dụng cho biến sau:
Phép gán là một biểu thức có dạng:
<tên_biến> := <biểu thức>;