Đặc tả và chứng minh tính đúng đắn của thiết kế cho các hệ đa tác tử chuyên ngành bảo đảm Toán học cho Máy tính và Hệ thống tính toán [Mã số : 60 46 35]

Abstract

Trình bày 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, đặc tả hệ thống đa tác tử. Trình bày về phương pháp kiểm chứng hệ thống đa tác tử bằng ngôn ngữ CafeOBJ, 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.