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

Tóm tắt Nghiên cứu về chứng minh tự động (Theorem Proving) trong CafeOBJ: ...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 g... 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ống 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 ...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...