I. Kiến thức cơ sở
Chương này giới thiệu các kiến thức nền tảng cần thiết để hiểu và xây dựng công cụ kiểm chứng tính nhất quán của mô hình phần mềm sau tái cấu trúc. Các khái niệm chính bao gồm ngôn ngữ ràng buộc đối tượng (OCL) và logic vị từ bậc nhất (FOL). OCL được sử dụng để biểu diễn các ràng buộc và hành vi của mô hình phần mềm, trong khi FOL là nền tảng toán học để kiểm chứng tính nhất quán. Chương cũng tổng quan về bài toán kiểm chứng tính nhất quán trong tái cấu trúc hệ thống phần mềm, nhấn mạnh sự cần thiết của việc đảm bảo tính nhất quán giữa các phiên bản trước và sau tái cấu trúc.
1.1 Ngôn ngữ ràng buộc đối tượng OCL
OCL là ngôn ngữ được sử dụng để biểu diễn các ràng buộc và hành vi của mô hình phần mềm. Nó được tích hợp vào UML để khắc phục các hạn chế của UML trong việc biểu diễn chi tiết các khía cạnh của thiết kế hệ thống. OCL có thể biểu diễn các ràng buộc bất biến, khởi tạo giá trị thuộc tính, tính toán giá trị dẫn xuất, truy vấn dữ liệu và tiền/hậu điều kiện của các phương thức. Ví dụ, OCL có thể được sử dụng để đảm bảo rằng tất cả các đối tượng của một lớp thỏa mãn một điều kiện nhất định.
1.2 Logic vị từ bậc nhất FOL
FOL là nền tảng toán học được sử dụng để kiểm chứng tính nhất quán của mô hình phần mềm. FOL cho phép biểu diễn các mệnh đề logic và kiểm tra tính đúng đắn của chúng. Trong đề tài này, FOL được sử dụng để chuyển đổi các biểu thức OCL thành các công thức logic, từ đó kiểm chứng tính nhất quán của mô hình phần mềm sau tái cấu trúc.
II. Xây dựng kiến trúc công cụ kiểm chứng
Chương này trình bày kiến trúc của công cụ CVT (Consistency Validator Tool), được thiết kế để kiểm chứng tính nhất quán của mô hình phần mềm sau tái cấu trúc. CVT bao gồm các thành phần chính như chuyển đổi biểu thức OCL sang FOL, kiểm tra tính tương thích của biểu thức OCL với mô hình UML, và kiểm chứng tính nhất quán giữa các phiên bản trước và sau tái cấu trúc. Công cụ này nhận đầu vào là các mô hình phần mềm và biểu thức OCL, sau đó thực hiện quá trình kiểm chứng và đưa ra kết quả.
2.1 Chuyển đổi biểu thức OCL sang FOL
Một trong những thách thức chính trong việc xây dựng CVT là chuyển đổi các biểu thức OCL phức tạp sang công thức FOL. Quá trình này đòi hỏi việc phân tích cú pháp và ngữ nghĩa của OCL để đảm bảo tính chính xác của việc chuyển đổi. CVT sử dụng các quy tắc chuyển đổi được xây dựng dựa trên cơ sở toán học của FOL để thực hiện công việc này.
2.2 Kiểm tra tính tương thích
CVT cũng thực hiện kiểm tra tính tương thích giữa các biểu thức OCL và mô hình UML. Điều này đảm bảo rằng các biểu thức OCL được sử dụng để mô tả hành vi của mô hình phần mềm là hợp lệ và phù hợp với cấu trúc của mô hình.
III. Cài đặt và thực nghiệm
Chương này mô tả quá trình cài đặt và thực nghiệm công cụ CVT trên hệ thống điều khiển giao thông đường bộ ARTC (Adaptive Road Traffic Control). CVT được cài đặt bằng ngôn ngữ lập trình Java và sử dụng Windows Builder/SWT để thiết kế giao diện người dùng. Quá trình thực nghiệm bao gồm việc kiểm chứng tính nhất quán của mô hình ARTC trước và sau tái cấu trúc, từ đó đánh giá độ tin cậy và hiệu quả của công cụ.
3.1 Cài đặt công cụ CVT
CVT được cài đặt bằng ngôn ngữ Java, với giao diện người dùng được thiết kế bằng Windows Builder/SWT. Công cụ này cho phép người dùng nhập các mô hình phần mềm và biểu thức OCL, sau đó thực hiện quá trình kiểm chứng tính nhất quán.
3.2 Thực nghiệm trên hệ thống ARTC
CVT được thử nghiệm trên hệ thống ARTC, một hệ thống điều khiển giao thông đường bộ. Quá trình thực nghiệm bao gồm việc kiểm chứng tính nhất quán của mô hình ARTC trước và sau tái cấu trúc. Kết quả thực nghiệm cho thấy CVT có khả năng phát hiện các vấn đề về tính nhất quán và đảm bảo tính chính xác của mô hình phần mềm sau tái cấu trúc.
