Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

i
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƢỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN
NGUYỄN QUỲNH CHI


Xin cảm ơn bạn bè, đồng nghiệp và nhất là các thành viên trong gia đình đã
tạo mọi điều kiện tốt nhất, động viên, cổ vũ tôi trong suốt quá trình học tập và
nghiên cứu để hoàn thành tốt bản luận văn tốt nghiệp này.
Nam định, Ngày 20 tháng 06 năm 2013
Học viên thực hiện

Nguyễn Quỳnh Chi

Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

iii LỜI CAM ĐOAN

Tôi xin cam đoan rằng, đây là kết quả nghiên cứu của tôi trong đó có sự giúp
đỡ rất lớn của thầy hướng dẫn và gia đình. Các nội dung nghiên cứu và kết quả
trong đề tài này hoàn toàn trung thực.
Trong luận văn, tôi có tham khảo đến một số tài liệu của một số tác giả đã
được liệt kê tại phần tài liệu tham khảo ở cuối luận văn.
Nam Định, Ngày 20 tháng 06 năm 2013
Học viên thực hiện
Viết tắt
Tên đầy đủ
MAS
Multi-Agent System
OTS
Observation Transition System
QLOCK
Locking with queue
Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

v Phụ lục

Giới thiệu 1
1.1 Đặt vấn đề 1
1.2 Nêu bài toán 3
1.3 Kết quả 3
1.4 Cấu trúc luận văn 4
Chương 2 5
Tổng quan về CafeOBJ 5
2.1 Giới thiệu 5
2.2 Đặc tả và kiểm chứng trong CafeOBJ 10
2.2.1 Ví dụ 10
2.2.2 Đặc tả số tự nhiên 11
2.2.3 Đặc tả thuộc tính 12

Hình 2.9 Chứng minh 0+j=j+0 16
Hình 2.10 Chứng minh lemma2: i + s(j) = s(i+j) 16
Hình 2.11 Chứng minh i+j = j + i 17
Hình 3.1 Mô tả bài toán Qlock 20
Hình 3.2. View of QLOCK 21
Hình 3.3 Mô hình QLOCK với OTS 22
Hình 3.4 Đặc tả (signature) cho hệ thống QLOCK 24
Hình 3.5 Đặc tả mô đun LABEL 25
Hình 3.6 Đặc tả mô đun PID 25
Hình 3.7 Kiểu biến tổng quát cho hàng đợi QUEUE 26
Hình 3.8 Hàng đợi QUEUE cho bài toán QLOCK. 27
Hình 3.9 Hành động want trong hệ thống QLOCK 28
Hình 3.10 Hành động try trong hệ thống QLOCK 28
Hình 3.11 Hành động exit trong hệ thống QLOCK 29
Hình 4.1 Kiểm tra giá trị của INV1 tại trạng thái init 31
Hình 4.2 Kiểm tra giá trị của INV1 với hành động want tại trạng thái s 32
Hình 4.3 Kiểm chứng INV1 với hành động want cho trường hợp ~(c-want) 32
Hình 4.4 Kiểm chứng INV1 với hành động want cho trường hợp (c-want) 33
Hình 4.5 Kiểm chứng INV1 với hành động want cho trường hợp (2) 34
Hình 4.6 Kiểm chứng INV1 với hành động want cho trường hợp (3) 35
Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

ii

Hình 4.7 Kiểm chứng INV1 với hành động want cho trường hợp (4) 36
Hình 4.8 Kiểm chứng INV1 với hành động want cho trường hợp (5) 36
Hình 4.9 Kiểm chứng istep1 với hành động want cho trường hợp (5) 37
Hình 4.10 Kiểm chứng istep 1 với hành động try cho trường hợp c-try (s,k) 38
Hình 4.11 Kiểm chứng istep 1 với hành động try cho trường hợp ~(c-try (s,k)) 38
Hình 4.12 Kiểm chứng istep 1 với hành động try cho trường hợp (2) 39

hai loại: đặc tả phi hình thức (ngôn ngữ tự nhiên) và đặc tả hình thức (dựa
trên kiến trúc toán học). Đặc tả phi hình thức là đặc tả sử dụng ngôn ngữ tự
nhiên. Tuy nó không được chặt chẽ bằng đặc tả hình thức nhưng được nhiều
người biết và có thể dùng để trao đổi với nhau để làm chính xác hóa các điểm
chưa rõ, chưa thống nhất giữa các bên phát triển hệ thống. Đặc tả hình thức là
đặc tả mà ở đó các từ ngữ, cú pháp, ngữ nghĩa được định nghĩa hình thức dựa
vào toán học. Đặc tả hình thức có thể coi là một phần của hoạt động đặc tả
phần mềm. Các đặc tả yêu cầu được phân tích chi tiết. Các mô tả trừu tượng
của các chức năng chương trình có thể được tạo ra để làm rõ yêu cầu.
Đặc tả phần mềm hình thức là một đặc tả được trình bày trên một ngôn
ngữ bao gồm: từ vựng, cú pháp và ngữ nghĩa được định nghĩa. Định nghĩa
ngữ nghĩa đảm bảo ngôn ngữ đặc tả không phải là ngôn ngữ tự nhiên mà dựa
trên toán học. Các chức năng nhận các đầu vào trả lại các kết quả. Các chức
năng có thể định ra các điều kiện tiền tố và hậu tố. Điều kiện tiền tố là điều
kiện cần thỏa mãn để có dữ liệu vào, điều kiện hậu tố là điều kiện cần thỏa
mãn sau khi có kết quả.
Có hai hướng tiếp cận đặc tả hình thức để phát triển các hệ thống tương
đối phức tạp:
-Tiếp cận đại số, hệ thống được mô tả dưới dạng các toán tử và các quan hệ
-Tiếp cận mô hình, mô hình hệ thống được cấu trúc sử dụng các thực thể toán
học như là các tập hợp và các thứ tự
Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

2

Kiểm thử một sản phẩm phần mềm là xây dựng một cách có chủ đích
những tập dữ liệu và dãy thao tác nhằm đánh giá một số hoặc toàn bộ các tiêu
chuẩn của sản phẩm phần mềm đó. Thử nghiệm có hai mục đích: chỉ ra hệ
thống phù hợp với đặc tả và phơi ra được các khuyết tật của hệ thố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


Yêu cầu là phải đảm bảo thiết kế đúng trước khi lập trình, nếu không lỗi
sẽ lan sang các bước sau và mất nhiều công hơn ( có thể là cấp mũ) mới tìm
được ra lỗi. Hiện nay vẫn còn làm thủ công, xem từng thiết kế so sánh với đặc
tả yêu cầu mới có thể tìm ra lỗi nên khó đảm bảo chất lượng. Một số sản
phẩm sẽ đòi hỏi chất lượng cao ( bằng phần mềm điều khiển) Vì không biết
trước số tác tử nên không biết được số trạng thái của hệ thống, ta coi không
gian trạng thái là hộp đen, nên không thể áp dụng các phương pháp kiểm
chứng bằng mô hình yêu cầu chứng minh lý thuyết không được làm thủ công,
ngược lại sẽ không nghiệm thu thiết kế. Khóa luận của tôi sẽ tập trung vào
chứng minh các thuộc tính của hệ thống đa tác tử bằng ngôn ngữ CafeOBJ; tư
tưởng chứng minh là dùng phương pháp qui nạp, phân rã bài toán ra các
trường hợp và thêm các bổ đề vào. Tư tưởng trên đã kiểm chứng được hệ
thống đa tác tử (MAS) với không gian trạng thái là vô hạn.
1.3 Kết quả
Luận văn đã đạt được các kết quả sau:
-Tìm hiểu và nắm rõ phương pháp đặc tả phần mềm sử dụng ngôn ngữ đại số
CafeOBJ.
Thu thập
yêu cầu
Đặc tả yêu
cầu
Lập trình

Thiết kế
Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

4

-Nắm vững phương pháp chứng minh tự động sử dụng tư tưởng qui nạp toán

2.1 Giới thiệu
CafeOBJ 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
con của kiểu khác. Ví dụ: số tự nhiên là thuộc số hữu tỉ, nhưng chúng đảm
bảo tính chất hợp lệ là 3 phải bằng 6/2.
-Lôgic biến đổi (Rewriting logic): Ngoài ra để bằng nhau, các biểu thức phải
hợp lệ tính đối xứng, chúng ta có thể sử dụng quan hệ bắc cầu. Đặc trưng của
quan hệ bắc cầu là rất thuận lợi để thể hiện đồng thời hoặc tính không xác
định.
-Các kiểu ẩn (Hidden sorts): Chúng ta có 2 loại trương đương. Một là tương
đương cực tiểu (minimal equivalence) chính là đồng nhất hóa 2 về và chúng
tương đương khi và chỉ khi chúng giống nhau thông qua các phương trình đã
cho. Kiểu tương đương khác dùng cho kiểu ẩn, là biến đổi 2 vế là tương
đương khi và chỉ khi chúng ứng xử đồng nhất dựa trên bộ quan sát đã cho.
Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

6

Đặc tả trong CafeOBJ bao gồm các mô đul, mỗi mô đun trong cafeOBJ
được định nghĩa với cú pháp
module module_name {
imports {
module_element …

Thành phần của module có thể được khai báo import, khai báo kiểu (sort),
khai báo toán tử (operation), khai báo biến, khai báo một phương trình
(equation), khai báo sự dịch chuyển (transition)
Định nghĩa kiểu (sort) trong CafeOBJ có cú pháp như sau:

Mô tả kiểu số nguyên không âm là kiểu con của kiểu số nguyên, định
nghĩa phép toán nhân hai số nguyên, phép chia một số nguyên cho một số
nguyên không âm. Để cung cấp sự mô tả các mô đun trong CafeOBJ, chúng ta tìm hiểu ví dụ
trong hình 2.2 với sự định nghĩa là mô đun BASIC-NAT như là mô tả số tự
nhiên, được lưu là nat+ps.mod; mô đun BASIC-NAT định nghĩa hai phép
toán 0 và s (next), định nghĩa thêm phép toán + và tính chất của phép toán 0
và s (next) bởi từ khóa eq.
[ sort-name sort-name ]

[ NzInt < Int ]
op _*_ : Int Int -> Int
op _/_ : Int NzInt -> Int

Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

8 file: nat+ps.mod

mod! BASIC-NAT {
imports {
Hình 2.3. Đọc file nat+ps.mod trong CafeOBJ
Để hiểu chi tiết hơn về cách chứng minh tính đúng đắn của đặc tả trong
CafeOBj ta dùng cú pháp:
CafeOBJ> set trace on
CafeOBJ> set trace whole on
CafeOBJ> thuộc tính cần chứng minh

Hình 2.4: Đọc chi tiết file cần chứng minh trong CafeOBJ
Với từ khóa eof trong CafeOBJ, chương trình sẽ chỉ đọc file đến dòng
trước từ eof, ở hình 2.5 chương trình sẽ chỉ đọc mod BASIC-NAT mà lờ đi
mod NATplus, và mô đun NATplus thừa kế mô đun BASIC-NAT
CafeOBJ> in nat+ps.mod
processing input : nat+ps.mod
defining module! BASIC-NAT+ _* done
CafeOBJ>

Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

10 file: nat+ps.mod

mod! BASIC-NAT {
protecting (NAT)


( I+ J) + K = I + (J + K), với I, J, K là số tự nhiên bất kỳ (*).
2.2.1.2 : Tính chất giao hoán của phép cộng các số tự nhiên
I+ J = J+ I , với I, J là số tự nhiên bất kỳ (**).
file: nat+ps.mod

mod! BASIC-NAT {
[ Nat] Mô tả kiểu biến là số tự nhiên “Nat”
op 0 : -> Nat Hằng số 0
op s_ : Nat -> Nat Phép toán tăng số tự nhiên
}

mod! NATplus {
pr(BASIC-NAT) Mô đun NATplus kế thừa mô đun BASIC-
NAT
op _+_ : Nat Nat -> Nat Phép cộng số tự nhiên
op _=_ : Nat Nat -> Bool {comm} - - Phép so sánh số tự nhiên
var M,N : Nat M, N Là các biến dùng để đặc tả
eq 0 + M = M . Biểu diễn quan hệ của các phép toán
cộng
eq (s M) + N = s(M + N) .
}
}
Hình 2.6. Mô đun BASIC-NAT trong CafeOBJ
2.2.2 Đặc tả số tự nhiên
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 BASIC-NAT trong
CafeOBJ như trong (hình 2.6). Đặ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, 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

> inductive step
**> induction hypothesis:
eq (i + j) + k= i + (j + k) .
**> conclusion of induction step proof for (s k):
red ((s i) + j) + k) = ((s i) + (j + k)) .
close
Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

13

Hình 2.8 : Chứng minh tính chất kết hợp của phép cộng các số tự nhiên
Sử dụng chương trình kiểm chứng bằng ngôn ngữ toán học CafeOBJ kết
quả của hình 2.8 trả về true, vậy thuộc tính (*) được chứng minh cụ thể như
sau:
**> Prove associativity: (i + j) + k = i +(j + k) chứng minh tính chất kết
hợp của phép cộng các số tự nhiên
> inductive base case proof for 0: Kiểm chứng với i = 0
red 0 + (j + k) = (0 + j) + k .
((0 + (j +k)) = ((0 + j) + k)
eq 0 + N = N
eq (0 + N:Nat) = N
N:Nat >(j +k)
VT = ((0 + (j + k)) = (J +k)
Eq (0 +N: Nat) = N
N: Nat -> j
VP: ((0 +j) + k) = (j + k)
VT = VP =>TRUE
**> conclusion of induction step proof for (s k): Chứng minh nó đúng với
(sk)
red ((s i) + j) + k = (s i) + (j + k) .

phương pháp quy nạp, đầu tiên kiểm chứng (**), với i=0, và giả thiết (**)
đúng với trường hợp i bất kỳ, sau đó chứng minh (**) đúng với s(i). Nhưng
khi red 0+ j = j + 0 không trả về giá trị true mà trả về một kiểu boolean, khi
đó ta phải thêm các bổ đề vào, làm sao để tìm ra bổ đề, ta nhận thấy trong mô
đun BASIC-NAT ta đã có tính chất eq 0 + M:Nat = M . Bây giờ nếu chứng
minh được bổ đề j+0=j với mọi j thì kết quả của 0+j=j+0 sẽ trả về true.
Sử dụng bổ đề trên ta sẽ chứng minh được j+0=0+j như hình sau
Hình 2.9. Chứng minh 0+j=j+0
Tiếp theo giả thiết i + j = j+i, khi red s(i) + j = j + s(i) không trả về true mà trả
về một kiểu boolean, có nghĩa là ta phải thêm bổ đề vào, vậy tìm bổ đề như
thế nào, nhận thấy từ BASIC-NAT ta có s(i) + j = s(i+j) theo giả thiết i+j=j+i
open (NATplus + EQL)
> declaring constants for induction
ops i j : -> Nat .
**> Prove Lemma1: i + 0 = i, by induction on i
**> induction base case (i = 0) : 0 + 0 = 0
red 0 + 0 = 0 .
**> induction step

nhiên Hình 2.11. Chứng minh i+j = j + i
opening module (NAT+ + EQL)
open (NATplus + EQL)
> declaring constants for induction
ops i j : -> Nat .
**> Prove Lemma2: i + (s j) = s(i + j) by induction on i
**> induction base case (i = 0) : 0 + (s j) = s(0 + j)
red 0 + (s j) = s(0 + j) .
**> induction step
eq i + (s J:Nat) = s(i + J) .
> conclusion of induction step
red (s i) + (s j) = s((s i) + j) .
**> should be true
**> QED for Lemma2
close

**> QED for Lemma2
close

**> Finally prove i + j = j + i
**> "again" by induction on i
**> induction base case (i = 0) : 0 + j = j + 0
reduce 0 + j = j + 0 .
**> induction step

trong OTS
- Phương thức OTS/CafeOBJ cung cấp một mô hình ngữ nghĩa và
framework chúng cho một hệ thống phức tạp.
Đặc tả và chứng minh tính đúng đắn hệ thống đa tác tử Nguyễn Quỳnh Chi

18

- Đối với việc kiểm chứng hình thức với một hệ thống bởi bộ
chúng được cung cấp bởi phương thức OTS/CafeOBJ.
Trong chương 2 trình bày về đặc tả và kiểm chứng trong CafeOBJ với hệ
thống đơn giản, trong khi thực tế có nhiều hệ thống phức tạp với sự chuyển
đổi trạng thái của hệ thống khi có một hoạt động nào đó tác động vào hệ
thống đó. Vì vậy với hệ thống biến đổi trạng thái trực quan (OTS) là một mô
hình hóa toán học sẽ giúp chúng ta dễ biểu diễn các đặc tả và kiểm chứng hệ
thống một cách chính xác và rõ ràng hơn.
3.2 Mô tả bài toán QLOCK
Ta thấy rằng nhiều tiến trình (agents or processes) tranh quyền sử dụng
một tài nguyên, nhưng tại một thời điểm chỉ có duy nhất một tiến trình có thể
sử dụng tài nguyên, vì thế mà tất cả các tiến trình phải tuân theo giao thức độc
quyền truy xuất (mutual exclusion protocol) trong việc sử dụng tài nguyên.
Trong đó QLOCK là một hệ thống sử dụng giao thức độc quyền truy xuất
với một hàng đợi (Queue) dùng chung cho tất cả các tiến trình (processes)
thỏa mãn các yêu cầu sau:
-Độc quyền truy xuất: Nếu tiến trình Pi đang sử dụng tài nguyên thì không
tiến trình nào được sử dụng , mà phải chờ cho tới khi tiến trình hiện thời kết
thúc.
-Tiến trình: Nếu không có tiến trình nào sử dụng tài nguyên và có một số
tiến trình muốn dùng thì một tiến trình nào đó phải được dùng.
-Trạng thái ban đầu: Mọi tiến trình không có nhu cầu sử dụng tài nguyên và
hàng đợi là rỗng.