ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Đậu Quốc Toản
NGHIÊN CỨU KHẢ NĂNG CHUYỂN ĐỔI
GIỮA CÁC ĐẶC TẢ HÌNH THỨC
VÀ ỨNG DỤNG TRONG KIỂM CHỨNG PHẦN MỀM
LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
HÀ NỘI-2015
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Đậu Quốc Toản
NGHIÊN CỨU KHẢ NĂNG CHUYỂN ĐỔI
GIỮA CÁC ĐẶC TẢ HÌNH THỨC
VÀ ỨNG DỤNG TRONG KIỂM CHỨNG PHẦN MỀM
Ngành: Công nghệ thông tin
Chuyên ngành: Kỹ thuật Phần mềm
Mã số: 60480103
LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
NGƯỜI HƯỚNG DẪN KHOA HỌC: TIẾN SĨ PHẠM NGỌC HÙNG
Lời cam đoan
Tôi xin cam đoan luận văn này là công trình nghiên cứu của riêng tôi. Các số
liệu, kết quả được trình bày trong luận văn là hoàn toàn trung thực và chưa
từng được công bố trong bất kỳ một công trình nào khác. Tôi đã trích dẫn đầy
đủ các tài liệu tham khảo, công trình nghiên cứu liên quan ở trong nước và quốc
tế. Ngoại trừ các tài liệu tham khảo này, luận văn hoàn toàn là công việc của
riêng tôi.
Hà Nội, 28 tháng 5 năm 2015
Học viên
Đậu Quốc Toản
iv
Tóm tắt
Assume-Guarantee Tool (AGTool) là một công cụ sinh giả định, có ý nghĩa quan
trọng trong việc giải quyết bài toán "bùng nổ không gian trạng thái" của phương
pháp kiểm chứng mô hình. Hiện tại, AGTool là một trong những công cụ tiềm
năng trong việc hỗ trợ kiểm chứng phần mềm hướng thành phần. Thay vì kiểm
chứng trên toàn bộ hệ thống, công cụ này chia bài toán kiểm chứng thành các
bài toán nhỏ hơn ứng với các thành phần phần mềm và kiểm chứng các thành
phần này một cách riêng biệt. Tuy nhiên, công cụ AGTool còn tồn tại nhiều hạn
chế để có thể ứng dụng vào trong thực tế và tương tác với các công cụ kiểm
chứng phần mềm khác như LTSA. AGTool sử dụng kiểu dữ liệu liệt kê (LF), đây
là một trong những kiểu biểu diễn của hệ thống dịch chuyển được gán nhãn (LTS).
Với mục đích tăng khả năng tương tác với các công cụ kiểm chứng phần mềm
khác, luận văn nghiên cứu sử dụng các tiến trình hữu hạn trạng thái (FSP) thay
thế cho kiểu dữ liệu LF của AGTool. Mục tiêu của luận văn là đưa ra phương
Model Checking
Kiểm chứng mô hình
AGV
Assume Guarantee Verifica- Kiểm chứng đảm bảo giả
tion
định
LTSA
Labeled Transition System Công cụ kiểm chứng hệ thống
Analyzer
tương tranh
Ocaml
Objective Caml
Ngôn ngữ lập trình hàm
OCaml
ML
Meta-Language
Siêu ngôn ngữ
LF
Listing Form
Dạng biểu diễn liệt kê của LTS
vi
Mục lục
1
Giới thiệu
1
2.3
Dẫn xuất . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7
2.4
Ghép nối song song . . . . . . . . . . . . . . . . . . . . . . . . . . .
7
2.5
LTS an toàn và thuộc tính an toàn . . . . . . . . . . . . . . . . . . .
8
2.6
Tính thỏa mãn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9
2.7
Đặc tả ngôn ngữ FSP . . . . . . . . . . . . . . . . . . . . . . . . . .
9
2.7.6
Tiến trình kết hợp . . . . . . . . . . . . . . . . . . . . . . . .
13
2.7.7
Tham số . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
14
2.7.8
Phép gán lại nhãn và phép ẩn . . . . . . . . . . . . . . . . .
15
2.7.9
Property, Progress và Menu . . . . . . . . . . . . . . . . . .
16
2.7.10 Biểu thức . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
16
vii
23
2.9.1
OCamllex . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23
2.9.2
OCamlyacc . . . . . . . . . . . . . . . . . . . . . . . . . . .
23
AGTool
25
3.1
Giới thiệu AGTool . . . . . . . . . . . . . . . . . . . . . . . . . . . .
25
3.2
Hạn chế của AGTool . . . . . . . . . . . . . . . . . . . . . . . . . .
27
33
4.2.1
Ý tưởng . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
4.2.2
Phân tích đánh giá . . . . . . . . . . . . . . . . . . . . . . .
36
4.2
5
Ngôn ngữ lập trình hàm OCaml . . . . . . . . . . . . . . . . . . .
Thực nghiệm
37
5.1
Cài đặt chương trình . . . . . . . . . . . . . . . . . . . . . . . . . .
37
2.1
Ví dụ của LTS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
2.2
Phương pháp biểu diễn liệt kê của LTS. . . . . . . . . . . . . . . .
6
2.3
Ví dụ của LF. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6
2.4
Ví dụ của FSP. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7
2.5
Ghép nối song song giữa INPUT và OUTPUT. . . . . . . . . . . .
8
11
2.12 Định nghĩa nhãn hành động. . . . . . . . . . . . . . . . . . . . . .
11
2.13 Định nghĩa tập các nhãn hành động. . . . . . . . . . . . . . . . . .
12
2.14 Định nghĩa Const, Range, Set. . . . . . . . . . . . . . . . . . . . . .
12
2.15 Định nghĩa tiến trình. . . . . . . . . . . . . . . . . . . . . . . . . . .
13
2.16 Định nghĩa tiến trình địa phương. . . . . . . . . . . . . . . . . . .
14
2.17 Định nghĩa thành phần tuần tự. . . . . . . . . . . . . . . . . . . . .
15
2.18 Định nghĩa thành phần tuần tự. . . . . . . . . . . . . . . . . . . . .
15
19
2.26 Định nghĩa biểu thức (tiếp). . . . . . . . . . . . . . . . . . . . . . .
20
2.27 Định nghĩa biểu thức (tiếp). . . . . . . . . . . . . . . . . . . . . . .
21
2.28 Ví dụ khai báo hàm. . . . . . . . . . . . . . . . . . . . . . . . . . . .
21
2.29 Ví dụ gọi hàm. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
21
2.30 Ví dụ hàm mức cao. . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
2.31 Ví dụ hàm nặc danh. . . . . . . . . . . . . . . . . . . . . . . . . . .
22
2.32 Ví dụ hàm đệ quy. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
26
3.3
Kết quả được sinh ra bởi AGTool. . . . . . . . . . . . . . . . . . . .
26
4.1
Kiến trúc của GUI-AGTool. . . . . . . . . . . . . . . . . . . . . . . .
28
4.2
Cấu trúc thành phần chuyển đổi từ FSP sang LF. . . . . . . . . . .
29
4.3
FSP M. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
29
4.4
Mô hình FSP Compiler. . . . . . . . . . . . . . . . . . . . . . . . . .
41
5.5
LTS của thành phần M2 . . . . . . . . . . . . . . . . . . . . . . . . .
41
5.6
LTS của thành phần P. . . . . . . . . . . . . . . . . . . . . . . . . .
41
x
DANH SÁCH HÌNH VẼ
5.7
LTS của thành phần M1 sinh ra bởi LTSA. . . . . . . . . . . . . . .
42
5.8
LTS của thành phần M2 sinh ra bởi LTSA. . . . . . . . . . . . . . .
Trong ngành công nghiệp phần mềm, việc đảm bảo chất lượng phần mềm là
một vấn đề quan trọng nhằm đảm bảo tính đúng đắn, giảm tỉ lệ lỗi, tìm khiếm
khuyết, v.v. của phần mềm trước khi đưa vào sử dụng [1]. Vấn đề này không chỉ
là yếu tố quyết định thành công của các công ty phần mềm trong việc nâng cao
uy tín và giảm chi phí bảo trì mà nó còn góp phần quan trọng tới sự thành công
của khách hàng. Vấn đề này càng cấp thiết hơn khi phát triển các phần mềm
nhúng/điều khiển. Lỗi trong phần mềm có thể gây ra thiệt hại không mong
muốn cho người sử dụng phần mềm hoặc có thể ảnh hưởng nghiêm trọng tới
tình hình kinh tế, chính trị, an ninh của quốc gia. Ví dụ, sự cố Therac-25 vào
khoảng giữa tháng 6 năm 1985 và tháng giêng năm 1987. Nguyên nhân của sự
cố này được xác định là do tương tác giữa các thành phần của hệ thống và lỗi
chương trình song song khi thực hiện một chức năng quan trọng của chương
trình [2, 3]. Sự cố này được xem như là tai nạn bức xạ tồi tệ nhất trong lịch sử
35 năm phát triển của ngành y học kể từ năm 1985 [2, 3]. Hơn nữa, trong tương
lai các tiện ích phục vụ cho con người đang dần được thay thế bởi các hệ thống
nhúng/điều khiển. Nên các hệ thống này sẽ trở nên phổ biến.
Để đảm bảo chất lượng phần mềm, hầu hết các công ty hiện nay sử dụng
các kỹ thuật kiểm thử trong đó chủ yếu là kỹ thuật kiểm thử hộp đen [1]. Tuy
nhiên, các kỹ thuật kiểm thử chỉ có thể phát hiện ra lỗi/khiếm khuyết chứ không
chỉ ra được phần mềm không còn lỗi. Một số dự án phần mềm hiện nay yêu cầu
phải chứng minh được tính đúng đắn của chương trình (đảm bảo rằng chương
trình không còn lỗi) trước khi đưa vào sử dụng. Điều này có nghĩa là chỉ áp
dụng phương pháp kiểm thử là chưa đủ để đảm bảo chất lượng phần mềm,
đặc biệt đối với những phần mềm yêu cầu tính đúng đắn và chất lượng cao
như : hệ thống điều khiển máy bay/tên lửa, hệ thống giám sát hạt nhân, v.v.
Một trong những phương pháp nhằm chứng minh tính đúng đắn của chương
trình đang được quan tâm nghiên cứu và áp dụng vào thực tế là kiểm chứng mô
1
nhập liệu trực quan và dễ dàng. Bên cạnh đó, GUI-AGTool cũng có khả năng
tương tác với các kiểu dữ liệu LF, FSP đơn giản. Những cải tiến này là một bước
tiến quan trọng trong quá trình đưa AGTool tiếp cận với thực tế và mở ra một
tiềm năng ứng dụng mới. Tuy nhiên, GUI-AGTool vẫn còn tồn tại nhiều vấn đề
cần được cải tiến. GUI-AGTool cần có khả năng sử dụng được kiểu dữ liệu FSP
hoàn chỉnh. Kết quả của quá trình chuyển đổi từ LF sang FSP cần được tối ưu
nhiều hơn.
Mục tiêu của luận văn này là đưa GUI-AGTool trở thành một công cụ làm
việc được với ngôn ngữ FSP hoàn chỉnh. Ý tưởng cơ bản của luận văn là nghiên
1 />2 />3 />
2
Chương 1. Giới thiệu
cứu đặc tả hoàn chỉnh của FSP và tích hợp GUI-AGTool với công cụ LTSA.
Những cải tiến này sẽ biến GUI-AGTool trở thành một công cụ hiệu quả và có
tính tương tác rộng rãi hơn trong thực tế.
Cấu trúc của luận văn được chia thành sáu phần. Chương đầu tiên giới
thiệu về vai trò của kiểm chứng phần mềm, công cụ hỗ trợ và bài toán cần giải
quyết trong luận văn này. Tiếp theo, chương 2 trình bày các khái niệm cơ bản
nhằm phục vụ luận văn. Chương này bao gồm các khái niệm về máy hữu hạn
trạng thái, dẫn xuất, ghép nối song song, thuộc tính an toàn, đặc tả của ngôn ngữ
FSP, ngôn ngữ lập trình hàm OCaml, Ocamllex và Ocamlyacc. Công cụ kiểm
chứng phần mềm dựa thành phần AGTool được mô tả ở chương 3. Những vấn
đề còn tồn tại của công cụ kiểm chứng AGTool được nêu ra trong chương này.
Các phương pháp chuyển đổi giữa các dạng biểu diễn của LTS được trình bày
trong chương 4. Trong chương này đưa ra hai phương pháp chuyển đổi qua lại
giữa hai cách biểu diễn của LTS là FSP và LF. Kết quả sau khi làm thực nghiệm
bằng công cụ GUI-AGTool được trình bày ở chương 5. Cuối cùng, chương 6 tóm
4
Chương 2. Kiến thức cơ bản
(a) LTS Input.
(b) LTS Output.
Hình 2.1: Ví dụ của LTS.
LTS Input được mô tả trực quan bởi Hình 2.1a. Khi hệ thống ở trạng thái 0
và thực hiện hành động in thì sẽ chuyển sang trạng thái 1, còn nếu hệ thống ở
trạng thái 1 thực hiện hành động send thì sẽ chuyển sang trạng thái 2.
LTS Output = Q2 , αM2 , σ2 , q20 , trong đó :
• Q2 = {0, 1, 2},
• αM2 = {send, ack, out},
• σ2 = {(0, send, 1), (1, send, 1), (1, out, 2), (2, ack, 0)},
• q20 = {0}.
LTS Output được mô tả trực quan bởi Hình 2.1b. Nếu hệ thống đang ở
trạng thái 1 mà thực hiện hành động send thì vẫn giữ nguyên trạng thái 1.
2.2
Các phương pháp biểu diễn LTS
Để chuẩn bị đầu vào cho các công cụ kiểm chứng mà các thành phần được đặc
tả bằng LTS, chúng ta biểu diễn LTS bằng một trong hai phương pháp sau.
(0,send,1),(1,out,2),(2,ack,0),0
(a) LF của tiến trình INPUT.
(b) LF của tiến trình OUTPUT.
Hình 2.3: Ví dụ của LF.
2.2.2
FSP
FSP là viết tắt của Finite State Processes (Các tiến trình hữu hạn trạng thái), là
một ngôn ngữ mô hình hóa biểu diễn tương ứng với LTS. FSP dùng để xây dựng
mô hình các tiến trình, nó có thể được phân tích và kiểm tra bởi công cụ LTSA
[3].
Nếu x là một hành động và P là một tiến trình thì kí hiệu ( x → P) thể hiện
cho một tiến trình thực hiện hành động x và sau đó chuyển sang trạng thái P.
Hình 2.4a biểu diễn tiến trình INPUT. Tiến trình này bao gồm các trạng thái
S0, S1, S2 và các hành động in, send, ack. Tiến trình INPUT được biểu diễn một
cách trực trực quan bởi Hình 2.1a. Hình 2.4b biểu diễn tiến trình OUTPUT. Tiến
6
Chương 2. Kiến thức cơ bản
trình này bao gồm các trạng thái S0, S1, S2 và các hành động send, out, ack. Tiến
trình OUTPUT được biểu diễn một cách trực quan bởi Hình 2.1b.
S0 = (in → S1),
là các dẫn xuất. Còn in in, in send send không phải là các dẫn xuất.
2.4
Ghép nối song song
Ghép nối song song (được ký hiệu là ) là phép toán ghép nối hai thành phần
phần mềm bằng cách đội bộ các hành động chung và gối đầu các hành động
còn lại [11]. Giả sử M1 = Q1 , αM1 , σ1 , q1 0 và M2 = Q2 , αM2 , σ2 , q2 0 , ghép
nối song song giữa M1 và M2 , ký hiệu M1 M2 được định nghĩa như sau. Nếu
M1 = Π hoặc M2 = Π thì M1 M2 = Π . Ngược lại, M1 M2 = Q, αM, σ, q0 ,
trong đó : Q = Q1 × Q2 , αM = αM1 ∪ αM2 , q0 = (q1 0 , q2 0 ) và hàm σ được xác
định như sau :
(i )
α ∈ αM1 ∩ αM2 , ( p, α, p ) ∈ δ1 , (q, α, q ) ∈ δ2
(( p, q), α, ( p , q )) ∈ δ
7
(2.4.1)
Chương 2. Kiến thức cơ bản
INPUT_OUPUT = (INPUT OUTPUT).
(a) FSP của INPUT||OUTPUT.
(b) LTS của INPUT||OUTPUT.
toàn p [3].
Thuộc tính an toàn Sa f etyProperty của một hệ thống được minh họa ở Hình
2.6. Thuộc tính này đảm bảo rằng khi hệ thống thực thi phải luôn đảm bảo các
hành động in và out phải được thực hiện đúng thứ tự in→out→in→out... Khi
hệ thống đang ở trạng thái 0 và thực hiện hành động out thì hệ thống sẽ dẫn tới
trạng thái -1. Trạng thái -1 được kí hiệu là trạng thái lỗi của hệ thống.
8
Chương 2. Kiến thức cơ bản
Hình 2.6: Biểu diễn LTS của thuộc tính an toàn Safety Property.
2.6
Tính thỏa mãn
Cho một LTS M, ta nói M thoả mãn thuộc tính p, ký hiệu M |= p, nếu và chỉ
nếu : ∀σ ∈ L( M) : (σ ↑ αp) ∈ L( p). Để kiểm chứng một thành phần M thoả
mãn một thuộc tính p, khi đó cả M và perr phải được biểu diễn dưới dạng của
LTS an toàn (Safety LTS), sau đó thực hiện phép toán ghép nối song song M perr .
Nếu LTS thu được sau phép ghép nối tồn tại một dẫn xuất có thể tới trạng thái
π, khi đó ta nói thành phần M vi phạm thuộc tính p. Ngược lại, M thoả mãn
thuộc tính p [3].
2.7
Đặc tả ngôn ngữ FSP
Định nghĩa FSP
FSPdescription:
FSPdefinition
FSPdescription FSPdefinition FSPdefinition:
ConstantDef
RangeDef
SetDef
ProcessDef
CompositeDef
PropertyDef
ProgressDef
MenuDef
FluentDef
AssertDef
Hình 2.9: Định nghĩa FSP.
Bên cạnh các định nghĩa dành cho tiến trình và kết hợp các tiến trình, một
mô tả FSP còn bao gồm các định nghĩa của các hằng số, dãy số nguyên, tập các
nhãn hành động, thuộc tính an toàn, thuộc tính progress, các menu, fluent và
assert. Các luật sinh mô tả FSP được định nghĩa trong Hình 2.9
2.7.2
Các định danh
Các định nghĩa FSP và các tham số tiến trình là các định danh bắt đầu bởi chữ
hoa. Nhãn hành động và các biến là các định danh được bắt đầu bằng chữ
thường [3]. Các luật sinh mô tả định danh được định nghĩa trong Hình 2.10
LowerCaseIdentifier Letter
LowerCaseIdentifier Digit
Letter:
UpperCaseLetter
LowerCaseLetter
Hình 2.11: Định nghĩa các chữ hoa, thường.
2.7.3
Nhãn hành động
Các hành động trong FSP được gán nhãn bởi các định danh thường hoặc bởi
một giá trị được kết hợp từ một biểu thức đóng kín bằng ngoặc vuông. Nhãn
hành động cũng được tạo nên bằng việc kết hợp các nhãn đơn giản hơn với một
dấu chấm ’.’ [3]. Nhãn hành động được đặc tả trong Hình 2.12.
ActionLabel:
LowerCaseIdentifier
ActionLabel . LowerCaseIdentifier
[Expression]
ActionLabel [Expression]
Hình 2.12: Định nghĩa nhãn hành động.
Ví dụ nhãn hành động: in [43] in[12] in[2][i*2] x[1].y[3].
Một tập các nhãn hành động được định nghĩa trong Hình 2.13.
Ví dụ tập các nhãn hành động: a,b,c X.a in[x:1..3] in[x:T] a.x,y,z.
11
Định nghĩa Const, Range, Set được đặc tả trong Hình 2.14 [3].
ConstantDef:
const ConstantIdent = SimpleExpression
RangeDef:
range RangeIdent = SimpleExpression .. SimpleExpression
SetDef:
set SetIdent = { setElements}
Hình 2.14: Định nghĩa Const, Range, Set.
Ví dụ:
const N = 3
range R = 0..N
set
S = {a,b,c,d[R]}
2.7.5
Định nghĩa tiến trình
Một tiến trình được định nghĩa bởi một hoặc các tiến trình địa phương. Tiến
trình có thể tùy chọn được tham số hóa, gán lại nhãn, ẩn hoặc mở rộng bảng
chữ cái [3]. Tiến trình được định nghĩa ở Hình 2.15. Tiến trình địa phương được
định nghĩa ở Hình 2.16.
12
Chương 2. Kiến thức cơ bản
ProcessDef:
(a -> S[3]),
STOP.
Thành phần tuần tự luôn được định nghĩa kèm với một tiến trình. Tiến
trình cuối cùng trong một thành phần tuần tự phải là END, STOP, ERROR hoặc
là tham chiếu tới một tiến trình địa phương. Thành phần kết nối các tiến trình
với trạng thái cuối của một tiến trình tuần tự được thay thế bởi trạng thái đầu
tiên của dãy tiến trình còn lại trong danh sách các tiến trình [3]. Hình 2.17 định
nghĩa thành phần tuần tự.
Ví dụ:
P(I=1) = (a[I]-> b[I] -> END).
SC = P(1);P(2);SC.
Tiến trình SC được định nghĩa trong ví dụ trên hoàn toàn tương đương với
tiến trình sau:
SC = (a[1] -> b[1] -> a[2] -> b[2] -> SC).
2.7.6
Tiến trình kết hợp
Tiến trình kết hợp được phân biệt với tiến trình chính bằng cách thêm tiền tố
vào trước định nghĩa. Các tiến trình kết hợp được tạo ra bằng cách sử dụng các
thành phần song song, gán lại nhãn, độ ưu tiên và phép ẩn. Gán nhãn và chia sẻ
13
Copyright: Tài liệu đại học ©