Luận văn: Sự đồng thuận của hệ thống đa thành phần

Ràng buộc thứ tự giữa các tiến trình tương tranh và sự đồng thuận của hệ thống đa thành phần

Nội dung tài liệu:

Luận án tập trung nghiên cứu và đề xuất các phương pháp để kiểm chứng chương trình tương tranh. Cụ thể, các phương pháp này được áp dụng ở hai giai đoạn chính: thiết kế và cài đặt mã nguồn chương trình. Ở giai đoạn thiết kế, phương pháp hình thức sử dụng Event-B được áp dụng để kiểm chứng bản thiết kế của chương trình Java tương tranh, nhằm phát hiện lỗi ở mức độ cao. Tiếp theo, để phát hiện lỗi ở mức độ thấp hơn, luận án đề xuất sử dụng phương pháp lập trình hướng khía cạnh kết hợp với bộ công cụ kiểm chứng mô hình JPF (Java PathFinder). Mục tiêu là kiểm chứng sự tuân thủ giữa bản cài đặt của chương trình Java tương tranh và đặc tả thiết kế của nó.

Luận án còn đề cập đến việc kiểm chứng sự đồng thuận của hệ thống đa thành phần, bao gồm cả ở giai đoạn thiết kế bằng Event-B và giai đoạn cài đặt mã nguồn Java (bytecode) bằng JPF. Các định nghĩa và bổ đề liên quan đến sự kiện hội tụ, sự kiện lấy giá trị hội tụ và sự đồng thuận của hệ thống đa thành phần được trình bày, làm cơ sở cho phương pháp đặc tả và kiểm chứng.