Tài liệu Khóa luận 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à...
45 trang |
Chia sẻ: haohao | Lượt xem: 1007 | Lượt tải: 0
Bạn đang xem trước 20 trang mẫu tài liệu Khóa luận Kiểm chứng mô hình phần mềm sử dụng NUSMV, để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên
ĐẠ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
KHỐ 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
KHỐ 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 khố 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à tồ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.
Ngồ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 tốn tử trong logic thời gian .......................................................9
3.2.1 Tốn tử globally (tồn thể) ............................................................9
3.2.2 Tốn tử next (tiếp theo) ...............................................................10
3.2.3 Tố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 tồ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 tố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 tố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 hồn tồ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 hồn tồ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ì ngồ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 hồn tồ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 hồn tồ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ĩ 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].
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
8
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. Sau đĩ sử dụng lệnh:
nusmv tên_file
trong đĩ tên_file là tên của file được viết bằng ngơn ngữ SMV.
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
9
Chương 3
Giới thiệu về logic thời gian
3.1 Khái niệm
Logic thời gian dùng để mơ tả các kí hiệu và hệ thống luật về giá trị đúng sai
của các vị từ cĩ tính đến yếu tố thời gian. Khác với logic mệnh đề trong đĩ mỗi
mệnh đề cĩ tính chất đúng sai rõ ràng mà khơng quan tâm đến thời điểm đang xem
xét, logic thời gian cho phép biểu diễn các mệnh đề mà giá trị chân lý của nĩ phụ
thuộc vào thời gian.
Một ví dụ: Với mệnh đề logic: Trời mưa. Theo logic vị từ, mệnh đề này luơn
đúng họăc luơn sai trong bất kì thời điểm nào. Tuy nhiên, giá trị đúng sai của nĩ cĩ
thể thay đổi theo thời gian. Cĩ thể ngày hơm nay trời mưa nhưng ngày mai trời
khơng mưa.
Nếu trong logic vị từ, mỗi vị từ chỉ cĩ thể cĩ một giá trị hoặc đúng (bằng 1)
hoặc sai (bằng 0) thì trong logic thời gian, mỗi vị từ được coi như một dãy các giá
trị mà mỗi phần tử của dãy chỉ cĩ thể cĩ giá trị đúng hoặc sai [9]. Nhờ đĩ, logic thời
gian cĩ thể biểu diễn được sự thay đổi theo thời gian của giá trị các biểu thức logic.
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 tốn tử trong logic thời gian
3.2.1 Tốn tử globally (tồn thể)
Tố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 tố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 Tốn tử next (tiếp theo)
Tố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)
Tốn tử next thường được kí hiệu bằng chữ cái X.
3.2.3 Tốn tử eventually (cuối cùng sẽ xảy ra)
Tố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. Tốn
tử ◊ được định nghĩa thơng qua tốn tử □ như sau:
◊ϕ ≡ □ φ
Tố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
nĩ.
CTL (branching-time-temporal logic): Logic thời gian rẽ nhánh. Thời
gian cĩ cấu trúc tuyến tính, mỗi trạng thái cĩ nhiều trạng thái ngay tiếp
sau nĩ.
Tĩm lại, nhờ khả năng xét đến yếu tố thời gian, temporal logic đã được sử
dụng rộng rãi trong cơng nghệ kiểm chứng phần mềm. Temporal logic thường được
sử dụng để mơ tả các thuộc tính cần kiểm chứng.
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
11
3.4 Sử dụng temporal logic để mơ tả một số thuộc tính cần
kiểm chứng
3.4.1 Safety (tính an tồn)
Tính an tồn của một chương trình đảm bảo rằng sẽ khơng bao giờ xảy ra tình
huống xấu trong chương trình (“something bad never happen”).
Tính an tồn cĩ thể được biểu diễn bằng temporal logic như sau:
AG ϕ trong CTL
hoặc
G ϕ trong LTL
Trong đĩ ϕ là một biểu thức logic.
Ví dụ của tính an tồn:
Nhiệt độ của phản ứng khơng bao giờ quá 100 độ C.
Bất kì lúc nào chìa khĩa xe chưa vặn tới vị trí khởi động, xe sẽ khơng
nổ máy.
3.4.2 Liveness (tính chạy được)
Thuộc tính liveness của một chương trình đảm bảo rằng nĩ cĩ thể thực thi
được một chức năng “tốt” nào đĩ đã đặt ra. (“something good will happen
eventually”).
Thuộc tính liveness cĩ thể được biểu diễn bằng các phép kết hợp AF hoặc F
trong temporal logic:
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 tố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
Ngơn ngữ SMV dùng để mơ tả các hệ thống hữu hạn trạng thái. Các kiểu dữ
liệu mà ngơn ngữ này cung cấp bao gồm: kiểu logic (boolean), kiểu số nguyên
(bounded interger subrange) và các kiểu dữ liệu liệt kê symbolic enum.
Các mơ tả của một hệ thống phức tạp cĩ thể được chia nhỏ thành các module
và mỗi một module này cĩ thể được thực thi nhiều lần.
4.2 Cấu trúc của chương trình viết bằng ngơn ngữ SMV
Một chương trình viết bằng ngơn ngữ SMV cĩ các phần như sau:
MODULE tên_module
VAR
Khai báo các biến.
ASSIGN
Mơ tả các bước chuyển trạng thái của hệ thống.
Kết thúc câu lệnh là một dấu chấm phẩy (;).
4.3 Các kiểu dữ liệu
4.3.1 Khai báo kiểu dữ liệu
Các mơ tả của một hệ thống phức tạp cĩ thể được chia nhỏ thành các module
và mỗi một module này cĩ thể được thực thi nhiều lần.
Một biểu thức khai báo biến cĩ định dạng như sau:
: ;
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
14
Trong đĩ là tên của biến cần khai báo, cịn là
kiểu dữ liệu của biến đĩ. Ví dụ, khai báo biến request với kiểu dữ liệu là boolean
như sau:
request : boolean;
4.3.2 Kiểu logic (boolean), kiểu số nguyên (integer) và kiểu liệt
kê (enum)
Kiểu logic chỉ chứa giá trị 0 hoặc 1. Ví dụ khi khai báo một biến logic:
var1:boolean
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’. Ngồ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 tố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:
: array .. of
Câu lệnh trên sẽ khai báo một mảng các phần tử cĩ kiểu là , chỉ
số của phần tử chạy từ đến . 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;
Tương đương với khai báo sau:
matrix[0] : array [2..0] of boolean;
matrix[1] : array [2..0] of boolean;
Kết quả, ta đã định nghĩa một ma trận với 2 hàng và 3 cột như sau:
matrix[0][0] matrix[0][1] matrix[0][2]
matrix[1][0] matrix[1][1] matrix[1][2]
Số chiều của mảng là khơng giới hạn.
Chú ý rằng một mảng trong ngơn ngữ SMV khơng hồn tồn là một kiểu dữ
liệu. Nĩ đơn giản chỉ là một tập hợp các biến đơn lẻ. Điều đĩ cĩ nghĩa là hồn tồn
cĩ thể định nghĩa một mảng chứa các phần tử cĩ kiểu dữ liệu khác nhau, bằng cách
khai báo giá trị của từng phần tử trong mảng. Ví dụ:
state[0] : {ready, willing};
state[1] : {ready, willing, able};
state[2] : {ready, willing, able, exhausted};
4.3.5 Kiểu cấu trúc
Kiểu cấu trúc của SMV cũng giống như của các ngơn ngữ lập trình như C,
Java ... Nĩ là một tập hợp các giá trị. Một biến cĩ kiểu cấu trúc cĩ thể được khai
báo như sau:
foo : struct {
c1 : kiểu_1;
c2 : kiểu_2;
...
cn : kiểu_n;
}
Trong đĩ c1, c2 ... cn là các tên biến. Khai báo trên tương đương với khai báo
sau:
foo.c1 : kiểu_1;
foo.c2 : kiểu_2;
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
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 tố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
tốn tác động đến từng phần tử đĩ. Ví dụ, xét trường hợp phép tố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 tốn khác là phép tố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
tốn tác động đến từng phần tử đĩ. Ví dụ, xét trường hợp phép tố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:
:= ;
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
17
Trong đĩ là một biểu thức kết hợp các biến và các phép tốn như
“~” và “&”. Sau khi thực hiện câu lệnh trên, biến ở vế trái sẽ cĩ giá trị bằng giá trị
của biểu thức ở vế phải. Ví dụ, với phép gán:
zip := foo & bar
với các giá trị của biến foo và bar ở trên ta được
zip := 0;0;0;1;...
Các phép gán trong ngơn ngữ SMV được thơng dịch đồng thời. Như vậy thật
ra hai phép gán liên tiếp nhau trong một chương trình khơng cĩ nghĩa là chúng được
thực hiện tuần tự. Ví dụ với hai phép gán trong một chương trình:
y := x + 1;
z := y + 1;
chúng ta cĩ z := x + 2;
4.5.2 Tĩan tử next
Các phép gán trong ngơn ngữ SMV được thơng dịch đồng thời. Như vậy thật
ra hai phép gán liên tiếp nhau trong một chương trình khơng cĩ nghĩa là chúng được
thực hiện tuần tự. Ví dụ với hai phép gán trong một chương trình:
Giả sử với x là một biến, khi đĩ next(x) sẽ là giá trị tiếp theo của x. Nĩi cách
khác, giá trị thứ i của next(x) bằng giá trị thứ (i+1) của biến x. Ví dụ:
x = 0, 1, 2, 3 ...
thì next(x) = 1, 2, 3, 4 ...
Bằng cách gán giá trị cho giá trị “next” của một biến, chúng ta cĩ thể định
nghĩa được một máy tuần tự. Ví dụ với x và y là hai biến kiểu logic, câu lệnh
next(x) := y ^ x;
định nghĩa một biến x mà sẽ đảo ngược mỗi khi biến y bằng 1. Theo định
nghĩa, (y^x) sẽ trả về giá trị bằng x nếu y sai và bằng ~x nếu y đúng. Tuy nhiên, vì
chưa khai báo giá trị khởi đầu của biến x nên chúng ta sẽ thu được những dãy khác
nhau tùy thuộc vào biến x khởi đầu là 1 hay là 0.
Chúng ta cĩ thể khai báo giá trị khởi đầu của biến x bằng câu lệnh như sau:
init(x) := 0;
Với giá trị khởi đầu này, giả sử với
y = 0; 1; 0; 1 ...
ta được
x = 0; 0; 1; 1; 0 ...
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
18
Mặt khác, nếu ta khai báo
init(x) := 1;
Ta được
x = 1; 1; 0; 0; 1 ...
4.6 Máy trạng thái
Chúng ta cĩ thể khai báo giá trị khởi đầu của biến x bằng câu lệnh như sau:
Một ví dụ về máy hữu hạn trạng thái: Trạng thái bắt đầu là “idle” và chờ đến
khi xuất hiện tín hiệu “start”. Trong chu kì tiếp theo, nĩ chuyển sang trạng thái
“cyc1”, tiếp đến là “cyc2”, rồi trở lại trạng thái “idle”. Ở trạng thái “cyc2”, nĩ tạo ra
tín hiệu “done”.
start,done : boolean;
state : {idle,cyc1,cyc2};
next(state) :=
switch(state){
idle: start ? cyc1 : idle;
cyc1: cyc2;
cyc2: idle;
};
done := (state = cyc2);
Đoạn mã trên cĩ sử dụng hai dạng câu lệnh rẽ nhánh. Tốn tử switch cũng
giống trong các ngơn ngữ lập trình như C hay Java. Trong trường hợp này nĩ nhận
đối số đầu vào là giá trị của biến state và nhảy đến nhánh cĩ gán nhãn là giá trị này.
Ví dụ, ban đầu biến state cĩ giá trị là idle, câu lệnh switch(state) sẽ nhảy đến câu
lệnh vế phải của nhãn idle.
Một câu lệnh rẽ nhánh khác sử dụng tốn tử “?”. Tốn tử này cũng tương tự
trong ngơn ngữ lập trình C. Ví dụ với câu lệnh:
Start ? cyc1 : idle
Nếu start là đúng thì trả về giá trị cyc1, ngược lại trả về idle.
Ngồi ra ngơn ngữ SMV cũng cĩ tốn tử if, then dùng để rẽ nhánh tương tự
như trong ngơn ngữ Pascal. Đoạn mã lệnh sau cũng tương tự đoạn mã lệnh phía
trên:
default done := 0;
in switch(state){
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
19
idle:
if start then next(state) := cyc1;
cyc1:
next(state) := cyc2;
cyc2:
next(state) := cyc2;
done := 1;
}
Tuy đoạn mã này cĩ chức năng giống hệt đoạn mã trước nhưng cĩ cấu trúc rõ
ràng và dễ đọc hơn.
Tĩm lại, ngơn ngữ SMV là một ngơn ngữ mơ tả một máy trạng thái hữu hạn
trong đĩ khơng cĩ những phụ thuộc vịng và chuyển trạng thái nhập nhằng. Ngơn
ngữ SMV cĩ thể dùng để thiết lập mơ hình dùng cho việc kiểm chứng.
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
20
Chương 5
Áp dụng NuSMV kiểm chứng mơ hình
phần mềm giả lập máy ATM
5.1 Đề xuất quy trình đặc tả và kiểm chứng phần mềm sử
dụng NuSMV
5.1.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. Khi đĩ,
kết quả kiểm chứng sẽ khơng cịn chính xác nữa. Ngồ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. Quy
trình sau được đưa ra với mục đích làm cho việc mơ hình hĩa trở nên dễ dàng và
đảm bảo độ chính xác cao.
Bản chất của ngơn ngữ SMV là một ngơn ngữ mơ tả một máy hữu hạn trạng
thái. Do đĩ một máy hữu hạn trạng thái và khơng cĩ các chuyển trạng thái lặp vơ
hạn thì sẽ ánh xạ tương ứng một mơ hình bằng ngơn ngữ SMV. 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.
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
21
5.1.2 Mơ tả quy trình
Mục tiêu của quy trình này là kiểm chứng phần mềm ở giai đoạn thiết kế hệ
thống. Việc kiểm chứng được thực hiện sau khi đã xây dựng được các biểu đồ trạng
thái của hệ thống cần xây dựng. Đố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.
Sau đây là diễn giải quy trình một cách chi tiết:
Bước 1: Xây dựng các đặc tả của hệ thống như thường lệ. Ở bước này
cần xác định rõ những thuộc tính cần kiểm chứng mà hệ thống địi hỏi.
Các thuộc tính này sẽ được sử dụng để biểu diễn bằng temporal logic
trong bước 3.
Bước 2: Thiết kế hệ thống. Bước này được thực hiện như thường lệ. Mục
tiêu của bước này là xây dựng được các biểu đồ trạng thái mơ tả hoạt
động của hệ thống cần xây dựng.
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. Các thuộc tính cần kiểm chứng đã được xác định trong bước 1
được đặc tả bằng temporal logic. Đư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.
5.2 Đặc tả và kiểm chứng mơ hình phần mềm giả lập máy
ATM
5.2.1 Đặc tả yêu cầu
5.2.1.1 Mơ tả bài tốn
Mục tiêu của quy trình này là kiểm chứng phần mềm ở giai đoạn thiết kế hệ
thống. Việc kiểm chứng được thực hiện sau khi đã xây dựng được các biểu đồ trạng
thái của hệ thống cần xây dựng. Đố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.
Để đơn giản và dễ hiểu cho việc minh họa phương pháp trên, chúng ta xét bài
tốn: Thiết kế một chương trình phần mềm mơ phỏng sự hoạt động của máy ATM.
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
22
Phần mềm này sẽ mơ phỏng một máy ATM. Máy ATM này cĩ một đầu đọc
thẻ, một màn hình hiển thị, một khe để xuất tiền, một máy in để in hĩa đơn, một
cơng tắc để tắt và bật tồn bộ máy ATM. Máy ATM sẽ giao tiếp với máy chủ của
ngân hàng qua mạng. Tuy nhiên phần giao tiếp với ngân hàng khơng đựơc xét đến
trong ví dụ này.
Mỗi lần sử dụng, khách hàng sẽ phải đưa thẻ ATM vào và nhập mã PIN. Dữ
liệu sẽ được kiểm tra. Sau đĩ khách hàng cĩ thể thực hiện một hoặc nhiều giao dịch.
Thẻ ATM sẽ vẫn ở trong máy cho đến khi người dùng khơng muốn thực hiện thêm
bất kì giao dịch nào nữa và chọn lấy lại thẻ, ngoại trừ trường hợp sẽ nĩi đến sau
đây.
Máy ATM sẽ cung cấp cho khách hàng những dịch vụ sau:
Khách hàng cĩ thể rút tiền từ tài khoản.
Khách hàng cĩ thể chuyển khoản.
Khách hàng cĩ thể xem số dư tài khoản.
Sau khi khách hàng chọn việc thực hiện một giao dịch, máy ATM sẽ chuyển
các dữ liệu về ngân hàng để kiểm tra. Nếu mã PIN của khách hàng khơng hợp lệ với
giao dịch đĩ, máy ATM sẽ yêu cầu khách hàng nhập lại mã PIN. Nếu khách hàng
nhập sai mã PIN ba lần, máy ATM sẽ giữ thẻ ATM và người dùng phải liên hệ với
ngân hàng để lấy lại thẻ.
Nếu giao dịch khơng được thực hiện thành cơng, máy ATM sẽ hiển thị một
thơng báo lỗi.
Sau mỗi giao dịch, máy ATM sẽ hiển thị thơng báo hỏi người dùng cĩ muốn
thực hiện giao dịch khác hay khơng.
Máy ATM cũng cĩ một cơng tắc khởi động để bật và tắt tồn bộ máy.
5.2.1.2 Các tác nhân của hệ thống
Hệ thống cĩ ba tác nhân sau:
Người điều hành: Người thực hiện các chức năng bật máy, tắt máy để bảo
trì hệ thống.
Người dùng: Người sử dụng hệ thống để thực hiện các giao dịch.
Ngân hàng: Cĩ vai trị kiểm tra thơng tin và phê duyệt các giao dịch được
hệ thống yêu cầu.
5.2.1.3 Mơ hình ca sử dụng tổng thể hệ thống
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
23
Nếu giao dịch khơng được thực hiện thành cơng, máy ATM sẽ hiển thị một
thơng báo lỗi.
Người điều hành cĩ thể bật máy hoặc tắt máy ATM để bảo trì. Trong một thời
điểm, máy ATM chỉ thực hiện được một phiên làm việc để phục vụ người dùng.
Phiên làm việc bao gồm nhiều giao dịch, tại đĩ người dùng cĩ thể thực hiện việc
chuyển tiền, rút tiền, vấn tin tài khoản. Trong mỗi giao dịch, máy ATM sẽ gửi yêu
cầu giao dịch đến ngân hàng. Ngân hàng sẽ xác minh lại thơng tin và quyết định phê
duyệt giao dịch đĩ hay khơng. Nếu trong lúc giao dịch, người dùng nhập sai mã PIN
nhiều lần thì máy ATM sẽ ngừng giao dịch đĩ lại và giữ lại thẻ của người dùng. Các
ca sử dụng này được mơ tả như trong hình sau:
Hình 5.1. Biểu đồ ca sử dụng hệ thống máy ATM.
5.2.1.4 Bật máy
Người bảo trì hệ thống ATM bật máy lên để máy ATM cĩ thể làm việc và
phục vụ khách hàng.
5.2.1.5 Tắt máy
Người điều hành
Người dùng
Ngân hàng
Bật máy
Tắt máy
Phiên làm việc
Giao dịch
Rút tiền Chuyển tiền Vấn tin tài khoản
Sai mã PIN
> >
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
24
Người bảo trì hệ thống tắt máy ATM, máy ATM ở trạng thái ngưng họat động
cho đến khi nào được bật lên.
5.2.1.6 Phiên làm việc
Máy ATM vào phiên làm việc. Một phiên làm việc bắt đầu khi khách hàng
đưa thẻ ATM vào khe đọc thẻ. Máy ATM đưa thẻ vào trong và đọc thẻ (nếu bộ đọc
thẻ khơng đọc được thẻ thì máy sẽ đưa thẻ ra). Hệ thống sẽ yêu cầu khách hàng
nhập mã PIN, sau đĩ hệ thống sẽ đưa ra một danh sách các loại giao dịch để khách
hàng lựa chọn. Sau khi một giao dịch đựơc thực hiện, hệ thống sẽ hỏi khách hàng cĩ
muốn thực hiện giao dịch nào khác hay khơng. Nếu khách hàng chọn khơng thực
hiện giao dịch nào nữa thì máy ATM trả lại thẻ cho khách hàng. Nếu một giao dịch
bị dừng do quá nhiều lần nhập sai mã PIN thì phiên giao dịch kết thúc và thẻ ATM
của khách hàng bị giữ lại trong máy.
Khách hàng cĩ thể kết thúc một phiên làm việc bằng cách ấn nút Cancel trong
khi đang nhập mã PIN họăc chọn một loại giao dịch
5.2.1.7 Giao dịch rút tiền
Rút tiền. Hệ thống sẽ yêu cầu người dùng chọn tài khoản muốn rút. Sau đĩ yêu
cầu người dùng chọn số tiền từ danh sách các số tiền cĩ thể rút. Hệ thống sẽ kiểm
tra xem hiện cĩ đủ tiền để thực hiện giao dịch hay khơng. Nếu đủ, hệ thống sẽ gửi
một yêu cầu phê duyệt tới ngân hàng, nếu khơng đủ, hệ thống sẽ yêu cầu người
dùng chọn số tiền khác. Sau khi yêu cầu rút tiền được ngân hàng phê duyệt, số tiền
tương ứng sẽ được đưa ra khỏi máy ATM cho người dùng và sau đĩ một hĩa đơn
được xuất ra.
Giao dịch rút tiền cĩ thể được dừng lại và bỏ qua nếu người dùng ấn nút
Cancel bất kì khi nào số tiền cần rút chưa được chọn.
5.2.1.8 Giao dịch chuyển tiền
Hệ thống sẽ yêu cầu người dùng chọn chuyển tiền từ tài khoản nào trong danh
sách tài khoản. Sau đĩ yêu cầu người dùng chọn một tài khoản để chuyển tiền tới.
Tiếp theo hệ thống yêu cầu nhập số tiền muốn chuyển. Sau đĩ hệ thống gửi yêu cầu
phê duyệt đến ngân hàng. Nếu yêu cầu chuyển tiền hợp lệ và được ngân hàng phê
duyệt, hệ thống sẽ thơng báo giao dịch thành cơng.
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
25
5.2.1.9 Giao dịch vấn tin tài khoản
Hệ thống hiển thị ra một danh sách các tài khoản và yêu cầu người dùng chọn
tài khoản cần vấn tin. Sau khi yêu cầu vấn tin được phê duyệt bởi ngân hàng, hệ
thống hiển thị thơng báo và in thơng tin tài khỏan cho người dùng.
5.2.1.10 Sai mã PIN
Trường hợp này xảy ra trong khi thực hiện giao dịch, ngân hàng kiểm tra
thơng tin và xác định mã PIN khơng đúng. Hệ thống sẽ dừng giao dịch hiện hành và
yêu cầu người dùng nhập lại mã PIN. Nếu mã PIN nhập lại đúng, giao dịch bị dừng
sẽ được tiếp tục thực hiện. Nếu mã PIN được nhập sai 3 lần thì hệ thống sẽ giữ lại
thẻ ATM của khách hàng và chấm dứt phiên làm việc.
5.2.2 Đặc tả các thuộc tính cần kiểm chứng
Về tổng thể hệ thống, 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).
Trong quá trình thực hiện một phiên làm việc, chúng ta muốn đảm bảo rằng,
sau khi đưa thẻ vào, cuối cùng nĩ phải được trả lại người dùng hoặc giữ lại trong
thẻ ATM.
Trong mỗi giao dịch, yêu cầu thực hiện giao dịch cần được gửi đến ngân hàng
để phê duyệt. Do đĩ chúng ta cần đảm bảo rằng, khơng cĩ giao dịch nào được thực
hiện hồn tất nếu trước đĩ nĩ chưa được gửi đến ngân hàng để phê duyệt.
5.2.3 Thiết kế hệ thống
Ở bước này, hệ thống được thiết kế. Sản phẩm của bước này là các biểu đồ
tương tác, biểu đồ trạng thái, biểu đồ lớp ... 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.
5.2.3.1 Biểu đồ trạng thái tổng thể hệ thống
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
26
Sau đây là biểu đồ trạng thái tổng thể hệ thống (bao gồm ca sử dụng bật máy
và tắt máy)
Hình 5.2. Biểu đồ trạng thái tổng thể hệ thống ATM.
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
Sau đây là 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:
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
27
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.
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
Sau đây là biểu đồ trạng quá trính thực hiện một giao dịch của hệ thống:
Đọc thẻ
Đọc mã PIN
Chọn giao dịch
Thực hiện giao dịch
Đưa thẻ ra
Dừng vì mã PIN nhập sai nhiều lần
Chọn giao dịch khác
Người dùng chọn “Kết thúc”
Giao dịch được chọn
Đọc mã PIN thành cơng
Đọc thẻ thành cơng
Thẻ khơng đọc được/ Hiển thị thơng báo “Thẻ khơng hợp lệ”
Nhấn nút Cancel
Nhấn nút Cancel
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
28
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.
5.2.4 Mơ hình hĩa hệ thống bằng ngơn ngữ SMV
5.2.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
Lấy thơng tin
Gửi thơng tin đến ngân hàng
Xử lý trường hợp sai
mã PIN
Hịan thành giao dịch
In hĩa đơn
Hỏi người dùng cĩ thực hiện
giao dịch khác khơng
Bỏ qua
Thơng tin được nhập vào
Mã PIN khơng đúng Ngân hàng phê duyệt
Mã PIN được phê duyệt
Bỏ qua in hĩa đơn
Chọn in hĩa đơn
Bỏ qua Nhập sai mã PIN nhiều lần
Ngân hàng khơng phê duyệt
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
29
VAR
state_overall: {TAT, CHO, PHUC_VU};
VAR
action: {BAT_MAY, TAT_MAY, KHOI_TAO_PHIEN_LAM_VIEC,
PHIEN_LAM_VIEC_HOAN_TAT, PHIEN_LAM_VIEC_BI_NGUNG};
ASSIGN
init(state_overall) := TAT;
init(action) := BAT_MAY;
next(state_overall) :=
case
(state_overall = TAT) & (action = BAT_MAY): CHO;
(state_overall = CHO) & (action = TAT_MAY): TAT;
(state_overall = CHO) & (action = KHOI_TAO_PHIEN_LAM_VIEC):
PHUC_VU;
(state_overall = PHUC_VU) & (action =
PHIEN_LAM_VIEC_HOAN_TAT): CHO;
(state_overall = PHUC_VU) & (action =
PHIEN_LAM_VIEC_BI_NGUNG): CHO;
1: state_overall;
esac;
Hình 5.5. 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). Thuộc tính này được mơ tả bằng CTL trong ngơn ngữ SMV như sau:
SPEC
AG((state_overall = TAT) -> EF(state_overall = PHUC_VU))
5.2.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
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
30
VAR
state_session: {DOC_THE, -- doc the
DOC_MA_PIN, -- doc ma PIN
CHON_GIAO_DICH, -- chosing transaction
THUC_HIEN_GIAO_DICH, -- performing transaction
TRA_LAI_THE, -- ejecting card
KET_THUC}; -- KET_THUC session and
not reject card
VAR
action_session: {THE_KHONG_DOC_DUOC, -- the khong doc duoc
DOC_THE_THANH_CONG, -- doc the thanh cong
NHAN_NUT_BO_QUA, -- nhan nut bo qua
DOC_MA_PIN_THANH_CONG, -- doc ma PIN thanh cong
GIAO_DICH_DUOC_CHON, -- giao dich duoc chon
KHACH_HANG_CHON_THUC_HIEN_GIAO_DICH_KHAC, -- khach hang chon
thuc hien giao dich khac
KHACH_HANG_CHON_KET_THUC, -- khach hang chon ket
thuc phien lam viec
NGUNG_VI_NHAP_MA_PIN_SAI_QUA_NHIEU}; -- ngung giao dich vi
nhap ma PIN sai qua nhieu
ASSIGN
init(state_session) := DOC_THE;
next(state_session) :=
case
-- reading card
(state_session = DOC_THE) & (action_session =
THE_KHONG_DOC_DUOC): TRA_LAI_THE;
(state_session = DOC_THE) & (action_session =
DOC_THE_THANH_CONG): DOC_MA_PIN;
-- reading pin
(state_session = DOC_MA_PIN) & (action_session =
NHAN_NUT_BO_QUA): TRA_LAI_THE;
(state_session = DOC_MA_PIN) & (action_session =
DOC_MA_PIN_THANH_CONG): CHON_GIAO_DICH;
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
31
-- choosing transaction
(state_session = CHON_GIAO_DICH) & (action_session =
NHAN_NUT_BO_QUA): TRA_LAI_THE;
(state_session = CHON_GIAO_DICH) & (action_session =
GIAO_DICH_DUOC_CHON): THUC_HIEN_GIAO_DICH;
-- performing transaction
(state_session = THUC_HIEN_GIAO_DICH) & (action_session =
KHACH_HANG_CHON_THUC_HIEN_GIAO_DICH_KHAC): CHON_GIAO_DICH;
(state_session = THUC_HIEN_GIAO_DICH) & (action_session =
KHACH_HANG_CHON_KET_THUC): TRA_LAI_THE;
(state_session = THUC_HIEN_GIAO_DICH) & (action_session =
NGUNG_VI_NHAP_MA_PIN_SAI_QUA_NHIEU): KET_THUC;
-- ejecting card
(state_session = TRA_LAI_THE) : KET_THUC;
1: state_session;
esac;
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.
Trong mơ hình này, chúng ta muốn đảm bảo rằng, sau khi đưa thẻ vào, cuối
cùng nĩ phải được trả lại người dùng hoặc giữ lại trong thẻ ATM (tức là hệ thống
phải đạt đến trạng thái END):
SPEC
AG ((state_session = DOC_THE) -> EF(state_session = KET_THUC))
5.2.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, -- lay thong
tin
GUI_THONG_TIN_DEN_NGAN_HANG, -- gui thong tin
den ngan hang
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
32
XU_LY_SAI_MA_PIN, -- chosing
transaction
HOAN_THANH_GIAO_DICH, -- hoan thanh giao
dich
THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG, -- thuc hien giao
dich khac hay khong
IN_HOA_DON, -- in hoa don
KET_THUC}; -- ket thuc
VAR
action_session: {
BO_QUA, -- an nut bo qua
THONG_TIN_DUOC_NHAP_VAO, -- thong tin duoc nhap vao hop
le
NGAN_HANG_KHONG_PHE_DUYET, -- ngan hang khong phe duyet
NGAN_HANG_PHE_DUYET, -- ngan hang phe duyet
MA_PIN_KHONG_DUNG, -- ma PIN khong dung
NHAP_SAI_MA_PIN_NHIEU_LAN, -- nhap sai ma PIN nhieu lan
MA_PIN_DUOC_PHE_DUYET, -- ma PIN duoc phe duyet
CHON_IN_HOA_DON, -- chon in hoa don
BO_QUA_IN_HOA_DON}; -- bo qua in hoa don
ASSIGN
init(state_transaction) := LAY_THONG_TIN;
next(state_transaction) :=
case
-- lay thong tin
(state_transaction = LAY_THONG_TIN) & (action_session =
BO_QUA): THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG;
(state_transaction = LAY_THONG_TIN) & (action_session =
THONG_TIN_DUOC_NHAP_VAO): GUI_THONG_TIN_DEN_NGAN_HANG;
-- gui thong tin den ngan hang
(state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) &
(action_session = NGAN_HANG_KHONG_PHE_DUYET):
THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG;
(state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) &
Kiểm chứng mơ hình phần mềm sử dụng NuSMV Nơng Gia Tự
33
(action_session = NGAN_HANG_PHE_DUYET): HOAN_THANH_GIAO_DICH;
(state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) &
(action_session = MA_PIN_KHONG_DUNG): XU_LY_SAI_MA_PIN;
-- xu ly sai ma PIN
(state_transaction = XU_LY_SAI_MA_PIN) & (action_session =
NHAP_SAI_MA_PIN_NHIEU_LAN): KET_THUC;
(state_transaction = XU_LY_SAI_MA_PIN) & (action_session =
BO_QUA): THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG;
(state_transaction = XU_LY_SAI_MA_PIN) & (action_session =
MA_PIN_DUOC_PHE_DUYET): HOAN_THANH_GIAO_DICH;
-- hoan thanh giao dich
(state_transaction = HOAN_THANH_GIAO_DICH) & (action_session
= CHON_IN_HOA_DON): IN_HOA_DON;
(state_transaction = HOAN_THANH_GIAO_DICH) & (action_session
= BO_QUA_IN_HOA_DON): THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG;
-- in hoa don
(state_transaction = IN_HOA_DON) :
THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG;
-- hoi nguoi dung co thuc hien giao dich khac hay khong
(state_transaction = THUC_HIEN_GIAO_DICH_KHAC_HAY_KHONG) :
KET_THUC;
1: state_transaction;
esac;
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.
Trong mơ hình này, chúng ta muốn đảm bảo rằng khơng cĩ giao dịch nào
được thực hiện mà trước đĩ dữ liệu khơng được gửi đến ngân hàng để phê duyệt:
!AG (!(state_transaction = GUI_THONG_TIN_DEN_NGAN_HANG) ->
EF(state_transaction = HOAN_THANH_GIAO_DICH))
5.2.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ế hồn tồn 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ự
34
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ự
35
Chương 6
Kết luận
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ế hồn tồ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.
Hướng phát triển tiếp theo của đề tài này cĩ thể là áp dụng NuSMV để kiểm
chứng mã nguồn phần mềm. 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.
Tài liệu tham khảo Nơng Gia Tự
36
Tài liệu tham khảo
[1] B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A Petit, L. Petrucci, P.
Schnoebelen. Systems and Software Verification: model-checking
techniques and tools, 2001.
[2] R. C. Bjork. An Example of Object-Oriented Design: An ATM Simulation.
[3] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine.
Kronos: A Model-Checking Tool for Real-Time Systems. Proceedings of the
10th international Conference on Computer Aided Verification (June 28 -
July 02, 1998). A. J. Hu and M. Y. Vardi, Eds. Lecture Notes In Computer
Science, vol. 1427. Springer-Verlag, London, 546-550.
[4] A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri. NuSMV: a new symbolic
model checker.
[5] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri,
R. Sebastiani, A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic
Model Checking. In Proceedings of the 14th international Conference on
Computer Aided Verification (July 27 - 31, 2002).
[6] E. M. Clarke, Orna Grumberg and Doron A. Peled. Model Checking. MIT
Press, 1999, ISBN 0-262-03270-8.
[7] H. Giese, Safety – Critical computer systems, AG Softwaretechnik, SCCS-
VI-6x, 2003.
[8] G. J. Holzmann. The Model Checker SPIN. IEEE Trans. Softw. Eng. 23, 5
(May. 1997), 279-295.
[9] Krưger, Fred, Merz, Stephan, Temporal logic and state systems, Springer,
2008. ISBN: 978-3-540-67401-6.
[10] M. Mansouri-Samani, S. Pasareanu, J. Penix, C. Mehlitz, O. Malley, C.
Visser, P. Brat, Z. Markosian and T. Pressburger. Program model checking:
A practitioner’s guide, Intelligent Systems Division NASA Ames Research
Center. April 27, 2007, pages. 31 – 45.
Các file đính kèm theo tài liệu này:
- LUẬN VĂN KIỂM CHỨNG MÔ HÌNH PHẦN MỀM SỬ DỤNG NUSMV.pdf