ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ

Phạm Ngọc Thắng

ĐẶC TẢ VÀ KIỂM CHỨNG PHẦN MỀM SỬ DỤNG
CafeOBJ

KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY

Ngành: Công nghệ thông tin

ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Phạm Ngọc Thắng
i
Lời cảm ơn

Em xin bày tỏ lòng cảm ơn sâu sắc tới TS. Nguyễn Việt Hà và ThS. Đặng Việt
Dũng về sự hướng dẫn, chỉ bảo tận tình, cùng với những lời khuyên quý giá của thầy
trong quá trình em học tập cũng như thực hiện khóa luận.
Em xin gửi lời cảm ơn tới các thầy cô giảng dạy tại Đại học Công nghệ - Đại học
Quốc Gia Hà Nội đã trang bị cho em những kiến thức quý báu trong thời gian em học
tại trường. Đó cũng là tiền đề cơ sở để em có thể thực hiện được tốt khóa luận của
mình.
Em xin gửi lời cảm ơn tới các thầy các cô trong bộ môn Công nghệ phần mềm đã
tạo điều kiện cho em được làm việc ở trên bộ môn với đầy đủ trang thiết bị cho em học
tập và làm việc.
Cảm ơn bạn bè, người thân về sự động viên, giúp đỡ về mặt tinh thần cũng như
về mặt vật chất trong thời gian em thực hiện khóa luận này.

Hà nội, tháng 6 năm 2010
Sinh viên thực hiện

Phạm Ngọc Thắng
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc Thắng
ii
Tóm tắt


Chương 3. Ngôn ngữ CafeOBJ 7
3.1 Giới thiệu 7
3.2 Đặc tả và kiểm chứng trong CafeOBJ 9
3.2.1 Ví dụ 9
3.2.2 Đặc tả số tự nhiên 10
3.2.3 Đặc tả thuộc tính 10
3.2.4 Kiểm chứng thuộc tính 10
Chương 4. Khái quát về OTS và bài toán QLOCK 13
4.1 Giới thiệu về OTS 13
4.2 OTS (Observation transition system) 14
4.3 Mô tả bài toán QLOCK 17
Đặc tả và kiểm chứng phần mềm sử dụng CafeOBJ Phạm Ngọc Thắng
iv
4.4 Đặc tả QLOCK với OTS 17
4.5 Đặc tả thuộc tính và kiểm chứng đặc tả 21
Chương 5. Đặc tả và kiểm chứng hệ thống lò vi sóng 24
5.1 Hệ thống lò vi sóng 24
5.1.1 Mô tả hệ thống 24
5.1.2 Mô tả các thuộc tính 26
5.2 Mô hình hóa hệ thống trong OTS/CafeObj 26
5.2.1 Mô hình hóa và mô tả hệ thống trong OTS 26
5.2.2 Đặc tả hình thức hệ thống trong CafeObj 28
5.2.3 Không gian trạng thái của hệ thống đặc tả hình thức 29
5.2.4 Các thuộc tính được mô tả 29
5.3 Kiểm chứng bằng phương pháp quy nạp 33
5.3.1 Các bước quy nạp 33
5.3.2 Kiểm chứng bằng phương pháp quy nạp trong CafeOBJ 33

Hình 5.7: Đặc tả các thuộc tính trong CafeOBJ 31
Hình 5.8: Mô đun ISTEP trong CafeOBJ 32
Chương 1: Giới thiệu Phạm Ngọc Thắng
1
Chương 1
Giới thiệu
1.1 Đặt vấn đề
Đặc tả và kiểm chứng hình thức là một pha quan trọng nhằm nâng cao độ tin cậy
và chất lượng của phần mềm sử dụng phương pháp hình thức. Đối với các hệ thống
yêu cầu độ tin cậy cao như hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển
tên lửa, … Các phương pháp đặc tả và kiểm chứng hình thức sẽ được áp dụng cho
những hệ thống này trước khi triển khai chúng. Trong khi việc kiểm thử phần mềm
(software testing) chỉ có thể chỉ ra các lỗi phát hiện được nhưng không thể chỉ ra được
phần mềm hoàn toàn không có lỗi, các phương pháp kiểm chứng có thể đảm bảo hệ
thống không có lỗi sau khi đã được kiểm chứng đúng đắn.
Hiện nay, đã có nhiều phương pháp và công cụ hỗ trợ cho việc đặc tả và kiểm
chứng phần mềm như OBJ [14], Maude [14], CafeOBJ [13], SPIN [15], SMV [17],
NuSMV [16], …. Mỗi phương pháp có những ưu và nhược điểm riêng và bị hạn chế
trong một số hệ thống nhất định.
Mục đích của khóa luận là tìm hiểu về phương pháp hình thức (formal method)
cũng như phương pháp đặc tả và kiểm chứng hình thức phần mềm trong CafeOBJ. Từ
mô tả của hệ thống cần kiểm chứng, chúng ta cần đặc tả hệ thống một cách hình thức
bằng ngôn ngữ CafeOBJ. Các thuộc tính cần kiểm chứng của hệ thống cũng được đặc
tả một cách tương tự. Sử dụng ngữ nghĩa cú pháp trong ngôn ngữ CafeOBJ để thể hiện
các đặc tả hệ thống cũng như các đặc tả thuộc tính của hệ thống cần kiểm chứng dưới
dạng hình thức từ các phát biểu của ngôn ngữ tự nhiên.
1.2 Nội dung nghiên cứu của khóa luận

kiếm (searching) các trạng thái.
Chương 6 tóm tắt kết quả đã đạt được, kết luận, những hạn chế và hướng nghiên
cứu phát triển trong tương lai.
Chương 2: Phương pháp hình thức Phạm Ngọc Thắng
3
Chương 2
Phương pháp hình thức
Trong ngành khoa học máy tính, phương pháp hình thức là các kỹ thuật toán học
cho việc đặc tả, phát triển và kiểm chứng các hệ thống phần mềm và phần cứng. Cách
tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng
hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, khi an toàn hay
an ninh có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống
sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của
quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được
sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.
2.1 Phân loại
Các phương pháp hình thức có thể được sử dụng tại nhiều mức:
Mức 0: Đặc tả hình thức có thể được thực hiện và rồi một chương trình được
phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này
có thể là lựa chọn hiệu quả nhất về mặt chi phí.
Mức 1: Sử dụng phát triển và kiểm chứng hình thức để tạo ra một chương trình
theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính
chất hoặc quá trình tinh chỉnh từ đặc tả hình thức tới một chương trình. Đây có thể là
lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí
vè an toàn và an ninh.
Mức 2: Sử dụng các bộ chứng minh định lý (theorem prover) để thực hiện các
chứng minh hình thức hoàn toàn và được kiểm chứng bằn máy móc. Việc này có thể

dụng để kiểm chứng xem các yêu cầu cho hệ thống đang được phát triển đã được đặc
tả một cách đầy đủ và chính xác hay chưa.
Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong
báo cáo ALGOL 60, John Backus đã trình bày một hệ thống ký hiệu hình thức để mô
tả cú pháp ngôn ngữ lập trình (sau này được đặt tên là Backus normal form hay
Backus-Naur form (BNF) (Dạng chuẩn tắc Backus)).

Chương 2: Phương pháp hình thức Phạm Ngọc Thắng
5
2.2.2 Phát triển
Khi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng
làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện
thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ:
Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ
thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy
được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp
cho việc dịch thẳng mã chạy được.
Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện
của đặc tả có thể trở thành các khẳng định trong mã chạy được.
2.2.3 Kiểm chứng
Khi một đặc tả hình thức đã được phát triển, đặc tả này có thể được dùng làm cơ
sở cho việc chứng minh các tính chất của đặc tả.
2.2.3.1 Chứng minh của con người
Đôi khi, động cơ cho việc chứng minh tính đúng đắn của một hệ thống không
phải là nhu cầu đảm bảo tính đúng đắn của hệ thống mà là mong muốn hiểu rõ hơn về
hệ thống. Do đó, một số chứng minh được thực hiện dưới hình thức chứng minh toán
học: viết tay hoặc đánh máy nội dung bằng ngôn ngữ tự nhiên, với mức độ phi hình

được các hệ thống này cũng ít hơn đòi hỏi cần thiết cho việc tạo ra các chứng minh
toán học tốt bằng tay. Nhờ đó, các kỹ thuật này có thể dùng được cho nhiều người hơn.
Những người phê phán cho rằng các hệ thống kiểu này giống như máy sấm
truyền: chúng đưa ra các tuyên bố về sự thật nhưng lại không đưa ra giải thích nào về
sự thực đó. Còn có cả vấn đề “kiểm định hệ kiểm định”; nếu chính chương trình tham
gia công tác kiểm định không được chứng minh là đúng, thì có thể có lý do để nghi
ngờ tính đúng đắn của các kết quả được tạo ra.
Bên cạnh các phê phán nội bộ nói trên, còn có các phê phán dành cho các
phương pháp hình thức. Với tầm phát triển hiện nay, các chứng minh về tính đúng đắn,
bằng tay hoặc bằng máy tính, đòi hỏi nhiều thời gian (và do đó cả tiền bạc) để được
tạo ra, với lợi ích hạn chế ngoài việc đảm bảo tính đúng đắn. Điều đó làm cho các
phương pháp hình thức thường chỉ được dùng trong các lĩnh vực thu được lợi ích từ
việc có được các chứng minh đó, hoặc sẽ gặp nguy hiểm nếu có lỗi không được phát
hiện.
Chương 3: Ngôn ngữ CafeOBJ Phạm Ngọc Thắng
7
Chương 3.
Ngôn ngữ CafeOBJ
3.1 Giới thiệu
CafeOBJ [5] [13] là một ngôn ngữ đặc tả đại số được phát triển ở Nhật Bản dưới
sự chỉ đạo của GS Kokichi Futatsugi trong phòng thí nghiệm Language Design tại
Viện khoa học và công nghệ tiên tiến Nhật Bản (JAIST). Chúng hỗ trợ phương pháp
kiểm chứng dựa trên kỹ thuật đặc tả đại số và phương pháp quy nạp nhằm kiểm chứng
các chương trình với miền trạng thái vô hạn. CafeOBJ là một ngôn ngữ thực thi dựa
trên nhiều cơ sở lôgic, chủ yếu dựa trên các đại số ban đầu và đại số được suy luận.
Các lôgic cơ bản của CafeOBJ bao gồm :
- Lôgic được sắp xếp theo thứ tự (Order-sorted logic): một kiểu có thể là kiểu

đun. Hình 3.1 Mô đun EXAMPLE trong CafeOBJ.

Để cung cấp sự mô tả một mô đun trong CafeOBJ, chúng ta tìm hiểu ví dụ trong
Hình 2.1, với sự định nghĩa mô đun EXAMPLE như là mô tả cho số tự nhiên. Mô đun
EXAMPLE thừa kế các kiểu (sorts) và các toán tử (operators) đã được định nghĩa
trong hai mô đun INT và NAT. Phần signature khai báo các kiểu Pnat, Nat và Int. Ký
hiệu “<” nghĩa là kiểu Nat là kiểu con của kiểu Int (chính là kiểu số tự nhiên là kiểu
con của kiểu số nguyên hay là kiểu số nguyên bao gồm cả kiểu số tự nhiên). Hằng số 0,
toán tử s được khai báo bởi op. Hành vi của toán tử “+” là được thực hiện bởi hai biểu
thức và được khai báo bởi eq.
module EXAMPLE{
imports {
protecting (NAT)
protecting (INT)
}
signature {
[PNat, Nat < Int]
op 0 : -> PNat
op s : PNat -> PNat
op (_+_) : PNat PNat -> PNat
}
axioms {
vars N M : Pnat
eq 0 + N = 0 .
eq s(M) + N = s(M + N) .
}
}

biểu diễn quan hệ của phép toán “=”
eq (X = X) = true .
eq (0 = s(Y)) = false .
eq (s(X) = s(Y)) = (X = Y) .
}

Chương 3: Ngôn ngữ CafeOBJ Phạm Ngọc Thắng
10
3.2.2 Đặc tả số tự nhiên
Như đã trình bày ở phần trên (mục 3.2.1), từ mô tả về số tự nhiên với ba phép
toán cơ bản, và các thuộc tính của nó. Chúng ta tiến hành đặc tả bài toán bằng mô đun
PNAT trong CafeOBJ như trong Hình 3.2. Đặc tả này định nghĩa các toán tử cần thiết
và các quan hệ giữa chúng cho ví dụ.
Trong đặc tả này, khai báo số tự nhiên kiểu [Nat], hằng số 0, các phép toán tăng
“s”, phép toán cộng “+”, phép so sánh “=”, được khai báo sau từ khóa op, cùng với các
phương trình biểu diễn quan hệ giữa chúng được khai báo sau từ khóa eq.
3.2.3 Đặc tả thuộc tính
Với đặc tả hệ thống PNAT như trên (Hình 3.2), chúng ta cần đặc tả thuộc tính
cần kiểm chứng (điều kiện (*)) như trong hình 3.3. Trong đó x, y, z là các hằng số tự
nhiên bất kỳ, hàm bất biến inv nhằm kiểm tra tính đúng đắn của thuộc tính (thỏa mãn
điều kiện (*)).

Hình 3.3: Đặc tả thuộc tính cho điều kiện (*).

3.2.4 Kiểm chứng thuộc tính
Như đã biết trong phần này chúng ta cần phải kiểm chứng thuộc tính hay chứng
minh điều kiện (*) thỏa mãn với mọi số tự nhiên bất kỳ. Nghĩa là chúng ta cần phải

chúng ta thấy được sự kiểm chứng qua hai trường hợp đó là trường hợp cơ sở và
trường hợp tổng quát. Sau Khi thực hiện chương trình như Hình 3.5 trong CafeOBJ, hệ
mod ISTEP{
pr(INV)
vars X Y Z : Nat
op istep : Nat Nat Nat -> Bool
eq istep(X, Y, Z) = inv(X, Y, Z) implies inv(s(X), Y, Z) .
} > Trường hợp cơ sở với x = 0
open INV
Kiểm tra
red inv(0,y,z) .
close
> Trường hợp tổng quát là chúng ta muốn chứng minh rằng:
giả sử inv(x,y,z) = true thì inv(s(x),y,z) = true
nghĩa là giả sử đặc tả đúng với x bây giờ chúng ta chỉ cần
chứng minh nó đúng với s(x) là được ).
open ISTEP
Kiểm tra
red istep(x,y,z) .
close

Chương 3: Ngôn ngữ CafeOBJ Phạm Ngọc Thắng
12
thống CafeOBJ đều trả về kết quả “true” trong cả hai trường hợp đó. Nghĩa là hệ


14
4.2 OTS (Observation transition system)
Chúng ta giả định rằng tồn tại một không gian trạng thái gọi là Y. Khi chúng ta
mô tả một hệ thống, hệ thống về cơ bản được mô hình hóa bằng cách quan sát các số
lượng chỉ liên quan đến hệ thống và quan tâm tới chúng từ bên ngoài của mỗi trạng
thái trong Y.
Một OTS S = <O, I, T> bao gồm:
- O: Tập hợp các quan sát. Mỗi quan sát o ∈ O là một hàm o : Y → D ánh xạ
tới từng trạng thái υ ∈ Y vào một số kiểu giá trị D (D có thể khác nhau cho
mỗi quan sát). Giá trị trả về bởi một quan sát (trong một trạng thái) được gọi
là giá trị của các quan sát (trong trạng thái).
Với một OTS S và hai trạng thái υ
1
, υ
2
∈ Y, sự bình đẳng giữa hai trạng
thái, ký hiệu là υ
1
=
S
υ
2
, đối với S được định nghĩa như sau:
υ
1
=
S
υ
2

1
, υ
1
') và
τ(υ
2
, υ
2
'), υ
1
’=
S
υ
2
'. τ có thể được coi là một hàm tương đương với Y đối với
=
S
. Vì vậy, τ(υ) được gọi là trạng thái tiếp sau của υ đối với τ.
Các điều kiện cτ cho một quy tắc chuyển đổi τ ∈ T được gọi là điều kiện có hiệu
quả. Với một trạng thái, giá trị chân lý của nó có thể được xác định bởi chỉ các giá trị
của các quan sát trong trạng thái. Các vị từ của loại này được gọi là các vị từ trạng thái.
Cho một trạng thái υ ∈ Y, cτ là đúng (true) trong υ, cụ thể là τ là hiệu quả trong υ,
khi và chỉ khi υ # S τ(υ).
Nhiều quan sát tương tự hoặc các quy tắc chuyển đổi có thể được lập chỉ mục.
Nói chung, các quan sát và các quy tắc chuyển đổi được biểu diễn băng o
i1
….
im
và τ
j1

thuộc tính an toàn đối với S khi và chỉ khi p là một trạng thái vị từ và p(υ) đúng cho
mỗi υ ∈ Υ.
Nếu chúng ta chứng minh rằng một OTS có thuộc tính an toàn p, theo phương
pháp quy nạp được sử dụng chủ yếu sau đây:
- Trường hợp cơ sở: Đối với bất kỳ trạng thái υ ∈ Υ trong đó mỗi quan sát o
∈ O thỏa mãn I, chúng ta thấy rằng p(υ) đúng.
- Bước quy nạp: Với bất kỳ trạng thái đạt được υ ∈ Υ sao cho p(υ) đúng,
chúng ta cho rằng, đối với bất kỳ quy tắc chuyển đổi τ ∈ T, p(τ(υ)) cũng
đúng.
Một OTS S được mô tả trong CafeOBJ. Không gian trạng thái Y được biểu thị là
một kiểu ẩn (hidden sort) Sys, bằng cách khai báo *[Sys]*.
Quan sát o
i1, …, im
∈ O được biểu thị là toán tử quan sát trong CafeOBJ. Chúng ta
giả định rằng các kiểu dữ liệu D
k
(k = i
1
, , i
m
) và D được mô tả trong đại số ban đầu và
có tồn tại các kiểu ẩn S
k
(k = i
1
, , i
m
) và S tương ứng với các kiểu dữ liệu. Các toán tử
quan sát CafeOBJ biểu thị o
i1, …, im

i1
, …, X
im
) .
Với X
k
(k = i
1
, , i
m
) là một biến trong CafeOBJ với S
k
, và f(X
i1
, …, X
im
) có
nghĩa là một hạng tử (bao gồm X
i1
, , X
im
) tương ứng với f(i
1
, …, i
m
).
Một nguyên tắc chuyển đổi τ
j1, ,jn
∈ T được biểu diễn bởi một toán tử hành động
trong CafeOBJ. Chúng ta giả định rằng các kiểu dữ liệu D

jn
), X
i1
, , X
im
)
= e-a(S, X
j1
, , X
jn
, X
i1
, , X
im
) if c-a (S, X
j1
, , X
jn
) .
Với e-a(S, X
j1
, , X
jn
, X
i1
, , X
im
) có nghĩa là một hạng tử (bao gồm S, X
j1
, ,

) = S if not c-a (S, X
j1
, , X
jn
) .
Nếu giá trị của o
i1, …, im
không bị ảnh hưởng bằng cách thực hiện τ
j1, ,jn
ở trạng
thái bất kỳ (bất kể giá trị chân lý của cτ
j1, ,jn
), phương trình sau đây được khai báo:
eq o (a (S, X
j1
X
jn
), X
i1
X
im
) = o (S, X
i1
, , X
im
) .
Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng

cs: get(Queue)

Chương 4: Khái quát về OTS và bài toán QLOCK Phạm Ngọc Thắng
18
Để khai báo hàng đợi tổng quát và định nghĩa cho phương thức “top” trong
QUEUE trước hết chúng ta tạo 2 mô đun (Hình 4.2) trong đó:
Mô đun EQTRIV thể hiện các phần tư khai báo tổng quát và mô đun OPTION
nhằm tiền định nghĩa cho phương thức “top” trong QUEUE. Khi một hàng đợi rỗng thì
phương thức “top” sẽ trả về hằng số none ngược lại sẽ trả về some(E) (Trong đó E
chính là phần tử ở đỉnh hàng đợi).

Hình 4.2: Kiểu biến tổng quát cho hàng đợi QUEUE.

Trong bài toán QLOCK chúng ta phải sử dụng một hàng đợi để thực hiện phương
thức độc quyền truy xuất cho cả hệ thống. Việc tạo ra một hàng đợi với các thuộc tính
và phương thức cơ bản của một hàng đợi như chúng ta đã biết, gồm các phương thức
put đưa một thành phần vào hàng đợi, phương thức get xóa một thành phần ra khỏi
hàng đợi và top lấy ra một thành phần trên đỉnh của hàng đợi. Các thuộc tính và những
phương thức cơ bản đó được định nghĩa trong CafeOBJ như Hình 4.3. Mô đun
QUEUE chính là đặc tả cho hàng đợi trong hệ thống QLOCK.
mod* EQTRIV{
[Elt]
op _=_ : Elt Elt -> Bool {comm}
}
mod! OPTION(X :: EQTRIV){
[Option]
op none : -> Option