Tóm tắt Luận án Phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện

Một trigger là một đoạn mã có cu pháp, không mã hóa nhưng không có ngữ nghĩa. Chính vì vậy, ta chỉ có thể kiểm tra liệu một trigger hoạt động có dẫn đến xung đột ràng buộc dữ liệu hay các triggers có thế dẫn đến các vòng lặp vô hạn không bằng cách thực thi chúng hoặc diều tra từng bước một. Vì những lý do này, các nghiên cửu về một khung làm việc hình thức cho mô hình hóa và kiếm chứng các triggers CSDL là cần thiết. Thêm vào dó, nếu ta có thế chỉ ra rằng thực thi của các trigger là đúng ở thời điểm thiết kế thì nó có thế làm giảm chi phí phát triển các ứng dụng CSDL. Trong chương này, chúng tôi đề xuất một phương pháp mới dế mô hình hóa và kiếm chứng hệ thống CSDL có trigger sử dụng Event-B ở giai đoạn thiết kế. Y tương chính của phương pháp xuất phát từ sự tương dồng vè cơ chế hoạt dộng của trigger và sự kiện Event-B. Dầu tiên, chúng tôi dề xuất một tập luật dể chuyển dối một hệ thống CSDL có trigger sang mô hình Event-B. sau dó kiểm tra một cách hình thức liệu hệ thống có thỏa mãn ràng buộc dữ liệu và phát hiện các vòng lặp vô hạn bằng việc chửng minh các mênh đề cần chứng minh của máy Event-B. Ưu điểm của phương pháp là hệ thống CSDL có thế chuyến dối sang mô hình Event-B một cách trực tiếp. Các tính chất quan trọng dược chứng minh một cách toán học thông qua chứng minh mệnh dề cần chứng minh vì vậy tính đúng đắn của các tính chất này dược đảm bảo. Phương pháp này có giá trị vì nó đảm bảo được hệ thống tránh dược một số lỗi nghiêm trọng ở thời điếm thiết kế.