Nghiên cứu về chứng minh tự động (Theorem
Proving) trong CafeOBJ

Tạ Thị Thu Hiền

Trường Đại học Công nghệ
Luận văn Thạc sĩ ngành: Công nghệ phần mềm; Mã số: 60 48 10
Người hướng dẫn: TS. Phạm Ngọc Hùng
Năm bảo vệ: 2010

Abstract: Chương 1: Giới thiệu. Chương 2: Tổng quan về ngôn ngữ CafeOBJ, kỹ
thuật đặc tả và kiểm chứng phần mềm bằng phương pháp hình thức được sử dụng
trong CafeOBJ. Chương 3: Đặc tả hệ thống đa tác tử và các thuộc tính. Chương 4: Mổ
tả về phương pháp kiểm chứng hệ thống đa tác tử bằng ngôn ngữ CafeOBJ, với tư
tưởng quy nạp, có thể kiểm chứng với không gian trạng thái là vô tận. Chương 5: 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

Keywords: Ngôn ngữ lập trình; Phần mềm; Hệ thống đa tác tử

Content
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. Có thể chia đặc tả phần mềm ra làm hai loại: đặc tả phi hình thức là đặc
tả dựa trên ngôn ngữ tự nhiên và đặc tả hình thức là đặc tả dựa trên kiến trúc toán học. Đặc tả
phi hình thức 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. Trong đặc tả hình thức các đặc tả yêu cầu được phân tích chi tiết, các

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êu bài toán
Bài toán thực hiện trong khóa luận là bài toán đặc tả và kiểm chứng hệ thống đa tác tử (MAS)
sử dụng ngôn ngữ CafeOBJ. Tài liệu [1] đã giải quyết được trường hợp xung đột tài nguyên,
tại một thời điểm chỉ có một tiến trình (agent) được sử dụng tài nguyên dùng chung. Khóa
luận của tôi sẽ tập trung vào chứng minh các thuộc tính khác 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:

3
- 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.
- Nắm vững phương pháp chứng minh tự động sử dụng tư tưởng qui nạp toán học
để kiểm chứng các thuộc tính bất biến (invariant property). Với phương pháp này,
để chứng minh một thuộc tính bất biến, chúng ta cần chứng minh nó đúng tại
trạng thái khởi tạo của hệ thống. Giả sử thuộc tính đúng tại một trạng thái bất kỳ s,
chúng ta phải chứng minh nó đúng với mọi trạng thái tiếp theo của s.
- Áp dụng những kiến thức đã tìm hiểu để kiểm chứng 04 thuộc tính của hệ thống
đa tác tử. Trong hệ thống này, các tác tử chia sẻ một tài nguyên dùng chung. Số
lượng tác tử trong hệ thống là vô hạn vì vậy không gian trang thái là vô hạn. Với
hệ thống này, chúng ta không thể áp dụng các phương pháp kiểm chứng mô hình
vì lý do trên. Kết quả kiểm chứng cho thấy hệ thống đa tác tử thỏa mãn các thuộc
tính cần kiểm tra tại mọi trạng thái của hệ thống.
1.4 Cấu trúc luận văn
Các phần còn lại của luận văn có cấu trúc như sau:

IFIP WG6.1 International Conference on Formal Methods for Open
Object-Based Distributed Systems (FMOODS 2003). Springer (2003).
[10] P. N. Hung, T. Aoki and T. Katayama: ``Modular Conformance Testing and
Assume-Guarantee Verification for Evolving Component-Based Software'', IEICE Trans.
on Fundamentals, Special Issue on Theory of Concurrent Systems and Its Applications,
Vol. E92-A, No.11, pp. 2772-2780 (2009)