ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ĐINH QUANG ĐẠT NGHIÊN CỨU PHƯƠNG PHÁP KIỂM CHỨNG MÔ
HÌNH PHẦN MỀM DỰA TRÊN SAT Ngành: Công Nghệ Thông Tin
Chuyên ngành: Công Nghệ Phần Mềm
Mã số: 60 48 10

TÓM TẮT LUẬN VĂN THẠC SĨ Hà Nội - 2013
1
Lời mở đầu
Ngày nay, với tốc độ phát triển cực kỳ nhanh của lĩnh vực công
nghệ thông tin tại Việt Nam và trên thế giới, nhất là đối với phần mềm
đã thâm nhập vào hầu hết các lĩnh vực của đời sống như mua bán (mua
hàng trực tuyến, các ứng dụng về kế toán, quản lý, . . . ), các lĩnh vực
ngân hàng (quản lý tài khoản, giao dịch tr ực tuyến, . ), các lĩnh vực
giải trí (trò chơi, phim ảnh, . . . ). Với sự bùng nổ về số lượng các phần

rất cơ bản, ví dụ, một hệ thống không nên đến được trạng thái mà ở đó
tiến trình không thể thực hiện (kịch bản của deadlock), và chủ yếu được
lấy từ đặc tả của hệ thống. Đặc tả này quy định những gì hệ thống phải
làm và những gì không, và do đó tạo nên cơ sở cho bất kỳ hoạt động
kiểm định nào. Một khuyết điểm được tìm thấy một khi hệ thống không
đáp ứng được một trong các thuộc tính của đặc tả. Hệ thống được xem
xét là "đúng" (correct) khi hệ thống thỏa mãn tất cả các thuộc tính lấy
từ đặc tả của hệ thống. Vì vậy, tính đúng đắn luôn luôn tương đối với
đặc tả, và không có một thuộc tính tuyết đối của hệ thống. Một sơ đồ
của kiểm định được mô tả trong hình 1.
Thiết kế
(Design)
Kiểm chứng
(Verification)
Đặc tả hệ thống
(System specification)
Sản phẩm/ bản thử
(Product/ Prototype)
Thuộc tính
(Properties)
Không tìm thấy
lỗi
Tìm thấy lỗi
Hình 1: Sơ đồ kiểm định hệ thống
1.1.3 Kiểm chứng mô hình
Kiểm chứng mô hình (Model Checking) là một kỹ thuật kiểm chứng
xem xét tất cả các trạng thái có thể của hệ thống theo cách vét cạn.
Tương tự như chương trình chơi cờ của máy tính kiểm tra những nước
đi có thể, model checker, công cụ giúp cho việc kiểm chứng mô hình,
xem xét tất cả các kịch bản hệ thống có thể xảy ra theo một cách có hệ

(Modeling)
Hình th c hóa
(Formalizing)
Hình 2: Sơ đồ tổng quan hướng tiếp cận kiểm chứng mô hình
1.1.4 Các tiến trình trong kiểm chứng mô hình
Trong việc áp dụng kiểm chứng mô hình để thiết kế các pha khác
nhau như sau:
• Pha Modeling:
– Mô hình hóa hệ thống dưới sự xem xét bằng cách sử dụng
ngôn ngữ mô tả mô hình của model checker bằng tay.
– Kiểm tra tính đúng đắn trước tiên và các đánh giá nhanh
của mô hình để thực thi một vài mô phỏng.
– Mô hình hóa các đặc tính để kiểm tra sử dụng ngôn đặc tả
các thuộc tính.
4
• Pha Running: chạy model checker để kiểm tra tính hợp lệ của
thuộc tính trong mô hình hệ thống.
• Pha Analysis:
– Thuộc tính có an toàn hay không? → kiểm tra thuộc tính
tiếp theo (nếu có thể);
– Thuộc tính có vi phạm hay không? →
∗ Phân tích phản ví du được sinh ra từ mô phỏng.
∗ Làm mịn mô hình, thiết kế, và các thuộc tính.
∗ Lặp lại toàn bộ thủ tục.
– Thoát ra khỏi bộ nhớ? → Cố gắng làm giảm mô hình và
thử lại.
1.1.5 Mặt mạnh và mặt yếu của kiểm chứng mô hình Mặt mạnh của
kiểm chứng mô hình:
• Áp dụng với một phạm vi rộng lớn các ứng dụng như các hệ
thống nhúng, công nghệ phần mềm và thiết kế phần cứng.

Một hệ thống dịch chuyển TS là một bộ (S, Act, −→, I, AP, L) với
• S là tập hợp các trạng thái,
• Act là tập hợp các hành động,
• −→⊆ S × Act × S là một quan hệ dịch chuyển,
• I ⊆ S là tập hợp các trạng thái khởi tạo,
• AP là tập hợp những mệnh đề nguyên tử, và
• L : S −→ 2
AP
là một nhãn của hàm.
6
T S được gọi là hữu hạn nếu S, Act, và AP là hữu hạn.
1.2.2 Logic thời gian
Đối với các hệ thống phản ứng (reactive systems), tính đúng đắn
phụ thuộc vào sự thực thi của hệ thống, không chỉ là đầu vào và đầu
ra của việc tính toán mà còn là vấn đề công bằng (fairness). Logic thời
gian là một hình thức vượt trội để xử lý các vấn đề này. Logic thời gian
mở rộng logic mệnh đề hoặc logic tân từ bằng cách cho phép chuyển
tới hành vi vô hạn của một hệ thống phản ứng. Chúng cung cấp các ký
hiệu một cách trực quan nhưng có một nền tảng toán học chính xác để
diễn tả tính chất về mối quan hệ giữa các nhãn trạng thái trong thưc thi.
Các hình thức cơ bản của thời gian được thể hiện trong phần lớn các
logic thời gian bao gồm hai toán hạng:
♢(hay còn được ký hiệu là F): cuối cùng trong tương lai.
(hay còn được ký hiệu là G): bây giờ và sau này trong tương lai.
1.2.2 Logic thời gian tuyến tính (LTL)
Lý luận của logic thời gian tuyến tính qua những dấu vết tuyến tính
theo thời gian. Ở mỗi thời điểm, chỉ có một lịch trình trong tương lai
thực sự xảy ra. Thông thường, lịch trình được định nghĩa như bắt đầu
ở “hiện tại” (now), trong các bước thời gian hiện hành, và tiến triển vô
hạn trong tương lai.

1.2.3 Logic tính toán cây CTL
Các công thức PTL khẳng định các thuộc tính của các hành vi đơn
lẻ, nhưng chúng cũng quan tâm đến giá trị của hệ thống: chúng ta nói
rằng công thức φ nắm giữ của T (viết là T |= φ) nếu φ nắm giữ của tất
cả các hoạt động của T . Theo nghĩa này, các công thức PTL biểu thị
các tính chất đúng đắn của hệ thống. Sự hiện diện của một hoạt động
thỏa mãn một thuộc tính nhất định không thể biểu thị trong PTL. Các
thuộc tính có khả năng như vậy thuộc về logic thời gian phân nhánh
như logic CTL. Trong mô hình thời gian nhánh, tại mỗi thời điểm t có
thể có rất nhiều khả năng trong tương lai. Với những khả năng tương
lai tương ứng là một đường đi được tổ chức từ t. Do đó, một đường đi
biểu diễn một khả năng xảy ra trong tương lai. Các toán tử thường biểu
thị hoặc là “A” nghĩa là với mọi khả năng trong tương lai diễn tả luôn
luôn, chắc chắn hoặc là “E” nghĩa là có thể tồn tại khả năng tương lai
diễn tả sự có thể, không chắc chắn.
Định nghĩa 1.4 Công thức mệnh đề CTL
Các công thức của mệnh đề CTL được định nghĩa quy nạp như sau:
- Mọi mệnh đề nguyên tử v ∈ V đều là công thức.
- Hợp của hai mệnh đề là một mệnh đề.
8
- Nếu φ và ψ là các công thức thì EXφ, EGφ, và φEUψ là các
công thức.
Định nghĩa 1.5 Quan hệ nắm giữ CTL
Quan hệ T , s |= φ được định nghĩa theo quy nạp như sau:
- T , s |= v (với v ∈ V) khi và chỉ khi v ∈ s(V).
- Ngữ nghĩa của phép hợp được định nghĩa như bình thường.
- T , s |= EXφ khi và chỉ khi tồn tại một s-path s
0
s
1

có sự tương ứng với AFAGφ(xem hình 3): mọi hoạt động của hệ thống
dịch chuyển T thỏa mãn FGp (hoặc là ở trạng thái s
0
mãi mãi hoặc là
kết thúc ở trạng thái s
2
), nhưng T , s
0
̸|= AFAG p (với hoạt động ở tại
trạng thái s
0
luôn luôn có những khả năng chuyển tới trạng thái s
1
).
p
¬ p
p
S
0
S
1
S
2
Hình 3: Một hệ thống dịch chuyển T mà T |= FGp nhưng T ̸|=
AFAGp.
Chương 2: Vấn đề bùng nổ trạng thái và giải quyết hướng cổ điển
9
2.1 Vấn đề của bùng nổ không gian trạng thái trong kiếm chứng
mô hình
Số lượng các trạng thái của một mô hình có thể rất to lớn. Một ví

cô đọng hơn so với các dạng chuẩn truyền thống, hơn nữa OBDDs có
thể thao tác rất hiệu quả.
Xem xét các công thức Boolean qua n biến x
1
, x
2
, , x
n
. Một lược đồ
quyết định nhị phân (BDD) là đồ thị có hướng không có vòng và có
một gốc với hai loại đỉnh là đỉnh kết thúc và đỉnh không kết thúc. Mỗi
10
đỉnh không kết thúc v được gán nhãn bởi một biến var(v) và có hai
phần tử kế tiếp, low(v) và high(v). Mỗi đỉnh kết thúc v được gán nhãn
bởi 0 hoặc 1 qua hàm Boolean value(v) Một BDD với gốc v xác định
một hàm Boolean f
v
(x
1
, , x
n
) theo cách sau:
• Nếu v là đỉnh kết thúc thì f
v
(x
1
, , x
n
) = value(v).
• Nếu v là đỉnh không kết thúc với var(v) = x

)

.
OBDD là một biểu diễn chính tắc của hàm Boolean. Điều này giúp
đơn giản hóa các tác vụ như kiểm tra hai công thức có tương với nhau
không và quyết định xem một công thức có thỏa mãn hay không. Biễu
diễn như vậy phải đảm bảo rằng hai hàm Boolean là tương đương một
cách logic khi và chỉ khi hai hàm Boolean có biểu diễn đẳng cấu. Hai
lược đồ quyết định nhị phân là đẳng cấu nếu tồn tại một song ánh H
giữa hai đồ thị sao cho:
• Các nút lá được ánh xạ tới các nút lá, và các đỉnh được ánh xạ tới
các đỉnh.
• Với mọi nút lá v, value(v) = value(H (v)).
• Với mọi đỉnh v:
• var(v) = var(H(v)).
• H(low(v)) = low(H(v)).
• H(high(v)) = high(H(v)).
Các Biểu đồ chuyển trạng thái có thể được thể hiện với các BDD như
sau. Trước tiên, phải thể hiện các trạng thái về n biến trạng thái Boolean
v = (v
1
, v
2
, , v
n
). Sau đó, thể hiện quan hệ chuyển R như công thức
Boolean về trạng thái các biến.
Biểu diễn chính tắc của các hàm Boolean có thể đạt được bằng cách
thay thế hai hạn chế trên cây quyết định nhị phân:
11

, v
′
1
, , v
′
n
).
với v
1
, , v
n
thể hiện trạng thái hiện tại và v
′
1
, , v
′
n
thể hiện trạng thái
kế tiếp. Cuối cùng, chuyển f
R
thành một BDD.
Thủ tục ToBDD lấy đầu vào là một công thức CTL f (v) và trả về là
một BDD thể hiện chính xác các trang thái của hệ thống thỏa mãn công
thức CTL. Các phép toán thời gian được xử lý như sau:
• T oBD D (EX f (v)) = ToBDD(∃v
′
. f
R
(v, v
′

trong các công cụ kiểm chứng dùng trong các ngành công nghiệp hiện
nay. Cho một hệ thống dịch chuyển trạng thái hữu hạn, một thuộc tính
logic thời gian, và giới hạn k, BMC sinh ra một công thức mệnh đề
thỏa mãn khi và chỉ khi thuộc tính có thể bị bác bỏ bởi phản ví dụ
của độ dài k. Công thức mệnh đề này dẫn tới một giải SAT (Boolean
satisfiability). Nếu không có phản ví dụ độ dài k được tìm thấy, thì tăng
giới hạn k và tìm xem có thấy phản ví dụ không. Với các thuộc tính
thỏa mãn (nghĩa là kiểm tra xem có thể tới được các trạng thái xấu hay
không), có thể chỉ ra rằng chỉ cần kiểm tra các phản ví dụ với độ dài
nhỏ hơn “diameter” của hệ thống ( số các dịch chuyển nhỏ nhất để tới
được tất cả các trạng thái của hệ thống). Hơn nữa, BMC có thể được
sử dụng để bắt các lỗi (hơn là kiểm chứng đầy đủ) bởi đơn giản chỉ cần
chạy với một độ dài phản ví dụ được cho hoặc với thời gian cho trước.
BMC có nhiều tiến bộ hơn so với kiểm chứng mô hình biểu trưng với
BDD:
1. BMC tìm các phản ví dụ nhanh hơn so với các hướng tiếp cận
dựa trên BDD.
2. BMC tìm các phản ví dụ của độ dài tối thiểu.
3. BMC sử dụng ít bộ nhớ hơn nhiều so với các hướng tiếp cận dựa
trên BDD.
4. BMC không yêu cầu người dùng chọn lựa sự sắp xếp các biến và
không cần thực hiện lại việc sắp xếp.
Trong BMC, các trạng thái của mô hình được thể hiện như các vectơ
của Boolean. Hệ thống chuyển dịch được mã hóa như sau:
• Tập hợp các trạng thái khởi tạo được quy định bởi một công thức
mệnh đề I(s), I(s) là true khi và chỉ khi s là một trạng thái khởi
tạo.
• Quan hệ dịch chuyển được quy định bởi một công thức mệnh đề
R(s, s
′

s
i
→ s
i+1
).
Sau đây, chúng ta mô tả BMC cho các thuộc tính an toàn LTL của dạng
G(p), vơi p là một mệnh đề nguyên tử.
3.1 Các thuộc tính an toàn
Thuộc tính Gp khẳng định rằng p là true trong tất cả các trạng thái
tới được. Chúng ta đạng mong muốn xác định xem có tồn tại một phản
ví dụ có chiều dài không lớn hơn giới hạn cố định k. Nói cách khác,
chúng ta mong muốn xác định xem liệu có tồn tại một đường dẫn tiền
tố hợp lệ (s
0
, , s
k
) trong đó p không đạt tại một vài trạng thái s
i
, với
i ≤ k. Do vậy, dãy (s
0
, , s
k
) là một phản ví dụ cho Gp khi và chỉ khi
công thức sau thỏa mãn:
I( s
0
) ∧
k−1


Boolean satisfiability (SAT) là một trong những vấn đề quan trọng
nhất của khoa học máy tính. SAT là bài toán quyết định xem có tồn tại
một thể hiện thỏa mãn với công thức Boolean đã cho. Nói cách khác,
các biến trong công thức Boolean được gán các giá trị làm cho công
14
thức có giá trị true. Quan trọng không kém là xác định không có phép
gán nào như vậy tồn tại. Tức là với tất các các phép gán biến đều cho
ra kết quả false. Trường hợp thứ hai, ta có thể nói rằng hàm là không
thỏa mãn. Ví dụ như công thức a ∧ b là thỏa mãn vì tồn tại phép gán
a = T rue và b = True để công thức a ∧ b = T rue .
Hầu hết các bộ giải công cụ SAT đều dựa trên thuật toán DPLL (Davis
Putnam Logemann Loveland). Thuật toán DPLL dựa trên tìm kiếm
theo chiều sâu của phép gán chân lý cục bộ với ba cải tiến bổ xung.
Sự giải thích cho ba cải tiến đó cho công thức CNF như sau:
• Kết thúc sớm: Một mệnh đề là true nếu có một literal là đúng.
Một mệnh đề là false nếu tất các các literal là sai.
• Xóa bỏ các pure literal: pure literal là các literal có cung dấu
trong tất cả các mệnh đề. Ví dụ như (A∨¬B), (¬B∨¬C), (A∨C),
A, B là các pure literal, C không phải là pure literal. Các pure
literal được gán giá trị true. Do đó, trong các mệnh đề thì các
pure literal sẽ được xóa bỏ.
• Lan truyền đơn vị: Mệnh đề đơn vị chứa một literal. Ví dụ như
nếu B = true thì (¬B ∨ ¬C) được rút gon thành ¬C và do đó C
phải được gán giá trị false. Nói chung, nếu tất cả literal là false
trừ một literal, thì literal đó phải là true.
3.3 Xác định giới hạn
Sử dụng hai phương pháp để xác định độ dài của phản ví dụ khi
kiểm chứng một thuộc tính an toàn như Gp. Lấy d là diameter của
hệ thống, tức là số bước đi nhỏ nhất để tới được tất cả các trạng thái.
Ngoài ra, d là số nhỏ nhất mà thỏa mãn: với mọi trạng thái s, nếu tồn

, s
i+1
) ∧ s = s
n
reach
≤n
(s) = ∃s
0
, , s
n
I( s
0
) ∧
n−1

i=0
R(s
i
, s
i+1
) ∧ (
n

i=0
s = s
i
)
Vị từ reach
=n
(s) nắm giữ khi và chỉ khi s có thể tới được trong chính

), nếu

k
i=0
R(s
i
, s
i+1
) nắm giữ
tru sau (q(s
0
) ∧ ∧ q(s
k
)) ⇒ q(s
k+1
) nắm giữ true.
3.2 BMC cho các thuộc tính LTL
Một phản ví dụ cho Fp chỉ có thể là một đường dẫn vô hạn. Để sử
dụng một đường dẫn tiền tố hữu hạn để thể hiện một đường dẫn vô hạn,
chúng ta xem xét tiềm năng của quay lui từ trạng thái cuối cùng của một
đường dẫn tiền tố hữu hạn tới một trạng thái trước đây, minh họa như
hình , một đường dẫn tiền tố hợp lệ (s
0
, , s
l
, , s
k
) có một quay lui từ
k tới l khi và chỉ khi quan hệ dịch chuyển R chứa cặp (s
k

) là một đường
dẫn tiền tố hợp lệ:
M
k
= I(s
0
) ∧
k−1

i=0
R(s
i
, s
i+1
)
Xem xét hai trường hợp sau. Trường hợp đầu tiên chuỗi (s
0
, , s
k
)
không có quay lui:
Với một giới hạn k và một chuỗi hữu hạn hoặc vô hạn π của k trạng
thái (s
0
, , s
k
), một công thức LTL f nắm giữ true theo π với giới hạn
k khi và chỉ khi π |=
0
k

k
f ∧ g khi và chỉ khi π |=
i
k
f và π |=
i
k
g.
17
π |=
i
k
X f khi và chỉ khi i < k và (π |=
i+1
k
f ).
π |=
i
k
F f khi và chỉ khi π |=
i
k
f ∨ XFf .
π |=
i
k
G f khi và chỉ khi π |= f ∧ XGf .
π |=
i
k

:= ¬p(s
i
) với p là một mệnh đề nguyên tử.
 f ∨ g
i
k
:= f 
i
k
∨ g
i
k
.
 f ∧ g
i
k
:= f 
i
k
∧ g
i
k
.
X f 
i
k
:=

 f 
i+1

∨ ( f 
i
k
∧ X( f Ug)
i
k
).
Với trường hợp có quay lui, xét một đường dẫn tiền tố (s
0
, , s
k
) với
quay lui từ k tới l. Xác định một đường dẫn vô hạn lasso π như hình :
π = (s
0
, , s
l−1
, sl, , s
k
, ). Xây dựng một công thức mệnh đề
l
 f 
0
k
nắm giữ khi và chỉ khi f nắm giữ trên π(trong ngữ nghĩa thông thường
LTL) như sau:
l
p
i
k

l
 f 
i
k
∧
l
g
i
k
l
X f 
i
k
:=

l
 f 
i+1
k
nếu i<k
l
 f 
l
k
nếu i=k
l
G f 
i
k
:=

i
k
∧

j−1
n=i
l
 f 
n
k

∨

i−1
j=l

l
g
j
k
∧

j−1
n=l
l
 f 
n
k

Sau khi có được định nghĩa chuyển dịch cho đường dẫn với cả hai

k
l=0
l
L
k
.
Biểu diễn M, f 
k
như sau:
M, f 
k
:= M
k
∧

(¬L
k
∧ f 
0
k
) ∨

k
l=0
(
l
L
k
∧
l

sự đóng góp mã cho các phần khác nhau của hệ thống. Một số công
ty, viện nghiên cứu và thương mại đã bày tỏ quan tâm hợp tác để phát
triển NuSMV. Các tính năng chính của NuSMV như sau: NuSMV cho
phép các thể hiện đồng bộ hoặc bất đồng bộ các hệ thống hữu hạn, và
phân tích các đặc tả thể hiện trong CTL và LTL, sử dụng kỹ thuật kiểm
chứng mô hình dựa trên BDD và SAT.
4.3 Thực nghiệm sử dụng NuSMV
Ví dụ thể hiện các yêu cầu người dùng của một hệ thống thư viện,
thể hiện dưới dạng biểu đồ lớp như 5:
Hình 5: Biểu đồ lớp các yêu cầu của hệ thống thư viện
Từ mô hình này có thể kiểm chứng thuộc tính như:
Một quyển sách(book) có thể được đặ trước(Reserve) chỉ khi nó đã
được mượn(Lend) hoặc sẵn sàng đặt trước(Reserve) bởi thành viên
khác(member).
hay một số thuộc tính khác trên bộ công cụ NuSMV.
Kết luận
Trong luận văn này tôi đã trình bày các kiến thức nền tảng của
kiểm chứng mô hình cũng như vấn đề của kiểm chứng mô hình. Các
tư tưởng, nội dụng để giải quyết vấn đề của kiểm chứng mô hình theo
cách tiếp cận cổ điển sử dụng BDD cũng như cách tiếp cận dựa trên bộ
giải công cụ SAT, đồng thời cũng giới thiệu về nguyên lý của bộ giải
20
công cụ SMT. Đây cũng là một hướng đi mới trong kiểm chứng mô
hình, đó là kiểm chứng mô hình dựa trên SMT thay vì sử dụng SAT
như hiện nay. Tác giả cũng mong muốn có thể phát triển luân văn tiếp
tục theo hướng này cũng như có thể kết hợp kiểm chứng mô hình với
các ngôn ngữ mô hình hóa thống nhất được sử dụng rộng tãi hiện nay
như UML. Đóng góp chính của luận văn bao gồm:
1 Tìm hiểu các vấn đề nền tảng trong kiểm chứng mô hình như
cách tiếp cận từ một vấn đề thực tiễn để đưa về bài toán kiếm