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

Abstract

Đặc tả và kiểm chứng là một trong những giải pháp quan trọng nhằm nâng cao chất lượng phần mềm. Có hai kĩ thuật được sử dụng phổ biến nhất hiện nay là kiểm chứng mô hình (Model Checking) và chứng minh tự động (Theorem Proving). Khác với kiểm chứng mô hình, chứng minh tự động có thể kiểm chứng với mô hình vô hạn trạng thái. CafeOBJ là một ngôn ngữ hỗ trợ đặc tả và kiểm chứng theo tư tưởng của chứng minh tự động. Mục tiêu của luận văn là nắm bắt và sử dụng cafeOBJ để đặc tả và kiểm chứng một số hệ thống điển hình trong thực tiễn. 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. - 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.