Kiểm chứng chương trình Java tuân thủ đặc tả UML bằng lập trình hướng khía cạnh

Abstract

Nghiên cứu ngữ nghĩa chuẩn của các biểu đồ tuần tự trong UML. Phương pháp phân tích và đọc định dạng XMI của các biểu đồ UML để trích ra các thông tin ngữ nghĩa và biến chúng thành các máy trạng thái xác định để kiểm chứng được thuận tiện. Nghiên cứu lập trình hướng khía cạnh và cài đặt chức năng kiểm chứng tự động các dãy lời gọi xem chúng có tuân thủ đặc tả hay không. Kết quả nghiên cứu là Thư viện đọc file XMI chứa các biểu đồ tuần tự theo chuẩn UML 2.0. Chương trình phát hiện các lỗi không tuân thủ đặc tả biểu đồ tuần tự UML 2.0 của chương trình. Cài đặt phương pháp kiểm tra tự động dựa trên AOP Đề xuất cách phân tích đặc tả biểu đồ tuần tự UML 2 và chuyển chúng thành máy trạng thái để kiểm chứng tính đúng đắn của chương trình tuân thủ đặc tả đó dựa trên lập trình hướng khía cạnh. Phương pháp đã được cài đặt dưới dạng công cụ phần mềm, có thể dùng để kiểm chứng ở mức dòng lệch. Đề xuất lý thuyết đã được công bố trong một bài báo khoa học tại hội thảo quốc tế (ACOMP2010)