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

Đặ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õ,...
Nội dung trích xuất từ tài liệu:
Báo cáo " Nghiên cứu về chứng minh tự động (Theorem Proving) trong CafeOBJ" 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ỆU1.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ấtlượ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à đặctả 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ữacá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ácmô 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 saukhi 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ự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ếttật của hệ thống. Trong khi việc kiểm thử phần mềm (software testing) [4] chỉ có thể chỉ racá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ácphươ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.Theo hướng tiếp cận mô hình, chúng ta có phương pháp kiểm chứng mô hình (Modelchecking) [3], với đầu vào là một otomat hữu hạn trạng thái và thuộc tính cần kiểm chứng, sẽcho kết quả đầu ra là true hoặc false. Hiện nay có nhiều phương pháp hỗ trợ đặc tả và kiểmchứng phần mềm theo hướng tiếp cận trên như SPIN [5], SMV [6], NuSMV [7] ... Khác vớikiểm chứng mô hình, chứng minh tự động (Theorem Proving) có thể kiểm chứng các hệ thốngvới mô hình là vô hạn trạng thái; CafeOBJ [2] là một ngôn ngữ hỗ trợ đặc tả và kiểm chứngtheo tư tưởng của chứng minh tự động.Mục đích của khóa luận là tìm hiểu về phương pháp đặc tả và kiểm chứng hình thức phầnmề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ốngmộ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ốngcũ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ướidạ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ánBà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óaluậ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ônngữ 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áctrườ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ả ...