ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN THẾ HUY

CHỨNG MINH TÍNH ĐÚNG ĐẮN CHO BÀI TOÁN
XUNG ĐỘT TÀI NGUYÊN CHO CÁC HỆ ĐA TÁC TỬ 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Ĩ
NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. PHẠM NGỌC HÙNG Hà Nội – 2014

i

LỜI CAM ĐOAN

Tôi xin gửi lời cảm ơn chân thành tới các thầy cô giáo khoa Công nghệ
thông tin, trường Đại học Công nghệ, Đại học Quốc Gia Hà Nội - nơi tôi đã
theo học trong thời gian qua. Các thầy cô đã cung cấp cho tôi những kiến thức
quý báu, tạo điều kiện tốt nhất cho tôi trong suốt quá trình học tập và nghiên cứu
tại trường.
Cuối cùng, tôi xin chân thành cảm ơn những người thân trong gia đình,
đặc biệt là bố mẹ tôi đã luôn động viên và ủng hộ tôi. Xin cảm ơn bạn bè cùng
khóa đã giúp đỡ tôi trong quá trình học tập.
Luận văn này được thực hiện với sự hỗ trợ của đề tài mã số QG.12.50 do
Đại học Quốc Gia Hà Nội tài trợ.

iii

MỤC LỤC
LỜI CAM ĐOAN i
LỜI CẢM ƠN ii
MỤC LỤC iii
BẢNG CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT ivv

Diễn giải
Tiếng Việt
1
AID
Agent Identification
Định danh tác tử
2
ATA
Airline Ticket Agent
Đại lý vé máy bay
3
FID
Flight Identification
Định danh chuyến bay
4
init
Initial state
Trạng thái khởi tạo
5
INV
Invariant
Bất biến
6
ISTEP
Inductive Step
Bước quy nạp
7
NAT
Natural Number
Số tự nhiên
v

DANH MỤC HÌNH VẼ
Hình 2.1: Định nghĩa mô-đun trong CafeOBJ. 4
Hình 2.2: Đặc tả mô-đun SIMPLE-NAT trong CafeOBJ. 4
Hình 2.3: Đặc tả mô-đun NAT+ trong CafeOBJ. 5
Hình 2.4: Hội thoại giữa CafeOBJ với người dùng. 5
Hình 2.5: Tổ chức các thành phần của một mô-đun. 6
Hình 2.6: Các công đoạn chứng minh tính chất (*). 7
Hình 3.1: Lưu đồ mô tả quá trình hoạt động của hệ thống cũng như tính chất độc
quyền truy xuất của các tác tử đối với mỗi tài nguyên. 9
Hình 3.2: Thao tác của hệ thống đối với mỗi hàng đợi tương ứng với mỗi tài
nguyên. 10
Hình 3.3a: Một số kịch bản của hệ thống. 11
Hình 3.3b: Một số kịch bản của hệ thống. 12
Hình 3.4: Định nghĩa tập hữu hạn các hành động của các tác tử 13
Hình 3.5: Định nghĩa đệ quy không gian trạng thái của hệ thống đa tác tử sử
dụng chung đa tài nguyên. 13
Hình 3.6: Định nghĩa thuộc tính bất biến của hệ đa tác tử sử dụng chung đa tài
nguyên. 14
Hình 3.7: Chứng minh thuộc tính bất biến luôn thỏa mãn. 14
Hình 3.8: Quy trình chứng minh các thuộc tính bất biến của hệ đa tác tử sử dụng
chung đa tài nguyên. 15
Hình 4.1: Mô hình hệ thống đại lý vé máy bay được mô tả trong hệ chuyển trạng
thái quan sát được – OTS. 17
Hình 4.2a: Phần đặc tả đầu tiên của mô-đun ATA. 18
Hình 4.2b: Đặc tả phương thức pc tại trạng thái khởi tạo của hệ thống (init). 19
Hình 4.2c: Đặc tả chi tiết cho phương thức queue tại trạng thái khởi tạo (init)

Hình 4.19: Kiểm chứng trường hợp not c-want(s,Fi,Ak) . 33
Hình 4.20: Kiểm chứng trường hợp 1 của phương thức try. 34
Hình 4.21: Kiểm chứng try với trường hợp 2. 35
Hình 4.22: Kết quả trả về của đoạn lệnh kiểm chứng try với trường hợp 2. 35
Hình 4.23: Phần đặc tả của bổ đề lemma1. 35
Hình 4.24: Bổ đề đúng đắn được rút ra từ lemma1. 35
Hình 4.25: Kiểm chứng try với trường hợp 2 sau khi áp dụng bổ đề đúng đắn
được rút ra từ lemma1. 36
Hình 4.26: Kiểm chứng try với trường hợp 3. 37
Hình 4.27: Kết quả trả về của đoạn lệnh kiểm chứng try với trường hợp 3. 37
Hình 4.28: Bổ đề đúng đắn được rút ra từ bổ đề lemma1. 37
Hình 4.29: Kết quả kiểm chứng try với trường hợp 4. 38
Hình 4.30: Kiểm chứng try với trường hợp 5. 38
Hình 4.31: Các trường hợp xem xét với want. 39
Hình 4.32: Các trường hợp xem xét với try. 40
Hình 4.33: Các trường hợp xem xét với exit. 40
1

Chương 1. GIỚI THIỆU
Kiểm chứng mô hình (model checking) [5, 6, 9] và các kỹ thuật kiểm thử
(testing) đang được xem là các giải pháp chủ yếu nhằm đảm bảo chất lượng cho
các sản phẩm phần mềm nói chung và các hệ thống đa tác tử nói riêng. Các kỹ
thuật kiểm thử chỉ có khả năng phát hiện ra lỗi hoặc khiếm khuyết của hệ thống
chứ không thể chỉ ra được hệ thống không còn lỗi. Do đó, nếu chỉ áp dụng các
kỹ thuật kiểm thử không thôi thì chưa đủ để đảm bảo chất lượng của hệ thống,
đặc biệt là đối với những hệ thống yêu cầu độ tin cậy cao. Để giải quyết vấn đề
này, một trong những phương pháp đang được áp dụng phổ biến là phương pháp
kiểm chứng mô hình. Hiện nay có nhiều phương pháp hỗ trợ việc đặc tả và kiểm
chứng phần mềm theo hướng tiếp cận mô hình như SMV [7], NuSMV [8], v.v.
Tuy nhiên, phương pháp kiểm chứng mô hình chỉ áp dụng được với các hệ

thống quản lý việc đặt vé máy bay của các đại lý vé máy bay là một ví dụ điển
hình cho một hệ thống đa tác tử sử dụng chung đa tài nguyên. Mô tả bài toán đặt
vé máy bay bằng ngôn ngữ tự nhiên và sau đó là mô tả bài toán này trong hệ
chuyển trạng thái quan sát được – OTS (Observational Transition System). Từ
đó, đặc tả và kiểm chứng tính đúng đắn cho hệ thống đại lý vé máy bay bằng bộ
chứng minh định lý CafeOBJ. Chương 5 là kết luận và định hướng phát triển
của đề tài. Phần cuối cùng là tài liệu tham khảo và phụ lục.
3

Chương 2. TỔNG QUAN VỀ CafeOBJ
2.1. Giới thiệu
CafeOBJ [3, 4] là một ngôn ngữ đặc tả đại số, có khả năng thực thi dựa trên
nhiều cơ sở lôgic khác nhau, phần lớn dựa vào các đại số ban đầu và các đại số
được suy diễn. Ngôn ngữ này hỗ trợ phương pháp kiểm chứng dựa trên các kỹ
thuật đặc tả đại số và phương pháp quy nạp toán học nhằm mục đích kiểm

ngôn ngữ CafeOBJ không phân biệt ba kiểu khai báo trên, tuy nhiên việc khai
báo rõ kiểu của mô-đun là rất cần thiết, nó giúp cho việc hiểu về đặc tả của mô-
đun đó một cách đầy đủ, chính xác, đặc biệt là đối với các hệ thống phức tạp.
Một mô-đun không có tham số trong CafeOBJ được khai báo với cú pháp
được trình bày như trong hình 2.1.
module module_name {
module_element *
}
Hình 2.1: Định nghĩa mô-đun trong CafeOBJ.
Chi tiết của định nghĩa mô-đun trong hình 2.1 như sau:
Module_name là tên của mô-đun cần định nghĩa, module_element là các
thành phần của mô-đun, thành phần của một mô-đun có thể là các khai báo của
việc kế thừa từ các mô-đun khác (import declaration), hoặc việc khai báo các
biến (sort declaration), hoặc việc khai báo các phép toán (operation declaration),
hoặc việc khai báo các biến (variable declaration), hoặc việc khai báo các
phương trình (equation declaration), hoặc việc khai báo các dịch chuyển
(transition declaration).
Chúng ta cùng xem xét hai ví dụ trong hình 2.2: Đặc tả mô-đun SIMPLE-
NAT và hình 2.3 : đặc tả mô-đun NAT+.
1: mod! SIMPLE-NAT {
2: [ Nat ]
3: op 0 : -> Nat { constr }
4: op s : Nat -> Nat { constr }
5: }
Hình 2.2: Đặc tả mô-đun SIMPLE-NAT trong CafeOBJ.
Chi tiết của khai báo trong hình 2.2 như sau:
Để khai báo và định nghĩa cho một mô-đun, đầu tiên ta khai báo kiểu của
mô-đun sau đó đến tên của mô-đun (dòng 1). Định nghĩa kiểu dữ liệu Nat (dòng
2), định nghĩa hằng số 0 thuộc kiểu dữ liệu Nat ta bắt đầu bằng từ khóa op (dòng
3), định nghĩa phép toán s (phép tăng một số tự nhiên lên 1 đơn vị) ta bắt đầu

defining module! NAT+ _ * done.
CafeOBJ>
Hình 2.4: Hội thoại giữa CafeOBJ với người dùng.
Để việc đặc tả được rõ ràng hơn, CafeOBJ hỗ trợ việc tổ chức các thành
phần của một mô-đun vào ba khối chính (blocks) là : khối imports – nơi khai
báo các mô-đun mà mô-đun hiện tại tham chiếu đến, khối signature - nơi định
nghĩa các kiểu dữ liệu và các phép toán, khối axioms – nơi khai báo các biến
6

(variables), các phương trình (equations), các dịch chuyển (transitions). Hình
2.5 mô tả chi tiết việc tổ chức các khối của mô-đun NAT+.
mod! NAT+ {
imports {
pr(SIMPLE-NAT)
}
signature {
op _+_ : Nat Nat -> Nat
}
axioms {
eq 0 + M:Nat = M .
eq s (N:Nat) + M:Nat = s (N + M) .
}
}
Hình 2.5: Tổ chức các thành phần của một mô-đun.
2.2. Đặc tả và kiểm chứng trong CafeOBJ
Sau khi đã đặc tả hệ thống và các thuộc tính của hệ thống, chúng ta bắt đầu với
công đoạn kiểm thử các thuộc tính có thỏa mãn với đặc tả hay không. CafeOBJ
hỗ trợ kiểm chứng theo phương pháp quy nạp toán học.
2.3. Ví dụ minh họa
Trong ví dụ này trình bày việc chứng minh tính chất kết hợp của phép cộng “+”


8

Chương 3. ĐẶC TẢ HỆ THỐNG ĐA TÁC TỬ SỬ DỤNG
CHUNG ĐA TÀI NGUYÊN
3.1. Giới thiệu bài toán
Một hệ thống có nhiều tài nguyên dùng chung, nơi có nhiều tác tử sử dụng
chung các tài nguyên đó. Tại một trạng thái bất kỳ của hệ thống, có thể có nhiều
tài nguyên khác nhau được sử dụng bởi nhiều tác tử khác nhau, đối với một tài
nguyên xác định thì chỉ có nhiều nhất một tác tử xác định được phép sử dụng tài
nguyên đó. Ta cần đặc tả hệ thống và thuộc tính của hệ thống để đảm bảo tính
đúng đắn cho vấn đề xung đột tài nguyên đối với các tác tử khi sử dụng chung
các tài nguyên đó.
Hệ thống có bao nhiêu tài nguyên thì cần có bấy nhiêu hàng đợi tương
ứng, các hàng đợi này sẽ dùng chung cho tất cả các tác tử. Mỗi hàng đợi sẽ ứng
với một tài nguyên, tác tử nào muốn sử dụng tài nguyên nào thì trước hết nó
phải tồn tại trong hàng đợi tương ứng với tài nguyên đó.
Với mỗi tác tử i bất kỳ khi tham gia vào hệ thống thì sẽ được hệ thống gán
cho nhãn rm, khi tác tử đang ở trong hàng đợi thì chúng có nhãn là wt, khi tác tử
đang sử dụng tài nguyên thì chúng có nhãn là cs. Việc gán nhãn cho mỗi tác tử
như vậy là để hệ thống quản lý được trạng thái của từng tác tử, từ đó ra quyết
định xử lý.
Ban đầu, với mỗi tác tử i khi tham gia vào hệ thống và chưa có nhu cầu sử
dụng tài nguyên thì được hệ thống gán nhãn là rm (tác tử đang ở miền dư). Khi

Theo mô tả đối với hệ thống như trên thì hệ thống cần thỏa mãn các yêu
cầu sau:
- Độc quyền truy xuất đối với mỗi tài nguyên: khi một tác tử có định
danh i bất kỳ đang sử dụng một tài nguyên bất kỳ của hệ thống thì
không một tiến trình có định danh j (j ≠ i) nào khác được sử dụng
tài nguyên mà i đang sử dụng.
- Đối với mỗi tác tử: nếu tại một thời điểm, một tài nguyên bất kỳ
của hệ thống chưa được sử dụng bởi bất kỳ tác tử nào và đang có ít
nhất một tác tử muốn sử dụng tài nguyên đó thì một tác tử trong số
đó phải được sử dụng tài nguyên.
- Đối với việc khởi tạo trạng thái ban đầu: mọi hàng đợi trong hệ
thống đều rỗng, mọi tác tử đều đang ở miền dư.
Chúng ta cùng xem xét một số kịch bản của hệ thống trên một hàng đợi
tương ứng với một tài nguyên bất kỳ.
Giả sử tại một trạng thái bất kỳ của hệ thống đang tồn tại ba tác tử có định
danh lần lượt là 1, 2 và 3 tham gia vào hệ thống, cả ba tác tử này đều muốn sử
dụng một tài nguyên có định danh là r
8
, hàng đợi tương ứng với r
8
là q
8
và chúng
11

đang ở miền dư rm. Ở trạng thái tiếp theo, khi tác tử 3 có nhu cầu sử dụng tài
nguyên (want
3
) thì hệ thống gán nhãn wt cho tác tử 3, thực hiện đẩy tác tử 3 vào
đuôi hàng đợi q

Hình 3.3a: Một số kịch bản của hệ thống.
12 Hình 3.3b: Một số kịch bản của hệ thống.
3.2. Phương pháp đặc tả
3.2.1. Đặc tả các tác tử
Hệ thống đa tác tử sử dụng chung đa tài nguyên cho phép đa tác tử thực hiện
việc truy xuất tài nguyên tại một trạng thái bất kỳ của hệ thống. Hệ thống quản
lý mỗi tài nguyên sao cho tại mỗi trạng thái bất kỳ của hệ thống trên mỗi tài
13

nguyên chỉ có duy nhất một tác tử truy xuất. Gọi RId là tập các định danh của
các tài nguyên, r là một tài nguyên bất kỳ, r ∈ RId.
Gọi AId là tập các định danh của các tác tử, RId là tập các định danh của
các tài nguyên và Sys là không gian trạng thái của hệ thống đa tác tử sử dụng
chung đa tài nguyên, với mỗi tác tử i ∈ AId, mỗi tài nguyên r ∈ RId, ta có tập
hữu hạn các hành động a
i1
, a
i2
, . . ., a
in
của các tác tử được định nghĩa như sau:
a
ij
: Sys × RId × AId → Sys với j = 1, , n
Hình 3.4: Định nghĩa tập hữu hạn các hành động của các tác tử
Với s ∈ Sys và con_a
ij

r ∈ RId, i ∈ AId, j ∈ [1 n] }
Hình 3.5: Định nghĩa đệ quy không gian trạng thái của hệ thống đa tác tử sử
dụng chung đa tài nguyên.
3.2.3. Đặc tả các thuộc tính bất biến
Trước khi triển khai một hệ thống nói chung và hệ đa tác tử nói riêng, có một số
thuộc tính của chúng mà ta cần kiểm chứng tính đúng đắn. Nghiên cứu này tập
trung giải quyết thuộc tính bất biến - thuộc tính phổ biến của các hệ thống nói
chung. Thuộc tính bất biến là tính chất mà hệ thống phải thỏa mãn tại mọi trạng
thái của hệ thống.
Đối với hệ thống này, thuộc tính bất biến được định nghĩa:
14

inv: Sys × RId × AId × AId → { true, false}.
Hình 3.6: Định nghĩa thuộc tính bất biến của hệ đa tác tử sử dụng chung đa tài
nguyên.
Để chứng minh một thuộc tính bất biến của hệ thống này luôn luôn thỏa
mãn, ta cần chứng minh được:
∀s ∈ Sys, ∀r ∈ RId, ∀i, j ∈ AId
Chứng minh: inv(s, r, i, j) = true.
Hình 3.7: Chứng minh thuộc tính bất biến luôn thỏa mãn.
3.3. Kiểm chứng hệ thống đa tác tử sử dụng chung đa tài nguyên
Hiện nay, để chứng minh tính đúng đắn của các hệ đa tác tử thì phương pháp
được áp dụng phổ biến là kiểm chứng mô hình [5, 6, 9]. Tuy nhiên, một trong
những hạn chế lớn nhất của kiểm chứng mô hình là vấn đề bùng nổ không gian
trạng thái khi áp dụng cho hệ thống lớn [9]. Vì lý do đó mà phương pháp kiểm
chứng mô hình khó áp dụng được trong thực tế. Mặt khác, phương pháp kiểm
chứng mô hình chỉ áp dụng được cho các hệ thống có không gian trạng thái hữu
hạn, nhưng các hệ đa tác tử có số lượng tác tử là không được biết trước hoặc vô
hạn thì không gian trạng thái của hệ thống có thể là vô hạn. Chính điều này đã
làm cho phương pháp kiểm chứng mô hình đối với các hệ đa tác tử là không thể

i, j ∈ AId}
Bước quy nạp:
{inv(s, r, i, j) = true | s ∈ Sys, ∀r ∈ RId,
∀i, j ∈ AId } →
{inv(a
kl
(s, r, k), r, i, j) = true | ∀r ∈ RId,
∀i, j, k ∈ AId, ∀l ∈ [1 n] }
Hình 3.8: Quy trình chứng minh các thuộc tính bất biến của hệ đa tác tử sử dụng
chung đa tài nguyên.
16

Chương 4. ĐẶC TẢ VÀ CHỨNG MINH TÍNH ĐÚNG
ĐẮN CHO HỆ THỐNG ĐẠI LÝ VÉ MÁY BAY
Ở chương 3 ta đã đặc tả các hệ đa tác tử sử dụng chung đa tài nguyên và
đề xuất phương pháp chứng minh các thuộc tính bất biến của hệ thống bằng
phương pháp quy nạp toán học. Trong chương này sẽ trình bày một ví dụ cụ thể
để minh chứng cho việc đặc tả và chứng minh tính đúng đắn của hệ thống đa tác
tử sử dụng chung đa tài nguyên.
Hệ thống đại lý vé máy bay là một hệ thống đa tác tử sử dụng chung đa tài
nguyên. Hệ thống cần quản lý nhiều đại lý vé máy bay (gọi tắt là đại lý) (đa tác

queue: Phương thức trực quan có giá trị trả về là hàng đợi tương ứng với
mỗi chuyến bay ở một trạng thái của hệ thống.
- Các phương thức chuyển trạng thái
want: Phương thức chuyển trạng thái được hệ thống thực hiện với nhãn
rm, phương thức này có giá trị trả về là trạng thái tiếp theo của hệ thống,
với ba tham số đầu vào có kiểu dữ liệu lần lượt là: Không gian trạng thái
của hệ thống, định danh của chuyến bay, định danh của tác tử.
try: Phương thức chuyển trạng thái được hệ thống thực hiện với nhãn wt,
phương thức này có giá trị trả về là trạng thái tiếp theo của hệ thống và ba
tham số đầu vào giống như phương thức want.
exit: Phương thức chuyển trạng thái được hệ thống thực hiện với nhãn cs,
phương thức này có giá trị trả về là trạng thái tiếp theo của hệ thống và ba
tham số đầu vào giống như phương thức want.

Hình 4.1: Mô hình hệ thống đại lý vé máy bay được mô tả trong hệ chuyển trạng
thái quan sát được – OTS.