Luận án tiến sĩ về khung hình thức đảm bảo chất lượng chuyển đổi mô hình - Nguyễn Thị Hạnh

DẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYÊN THỊ HẠNH KHUNG HÌNH THỨC HỖ TRỢ ĐẢM BẢO CHAT LƯỢNG CHUYEN DOI MÔ HÌNH LUẬN AN TIEN SĨ KY THUẬT PHAN MEM Hà Nội - 2023 DẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYÊN THỊ HẠNH KHUNG HÌNH THỨC HỖ TRỢ ĐẢM BẢO CHAT LUGNG CHUYEN DOI MÔ HÌNH Chuyên ngành Kỹ thuật phan mềm Mã số: 9480103.01 LUẬN ÁN TIEN SĨ KỸ THUẬT PHAN MEM NGƯỜI HƯỚNG DẪN KHOA HỌC: 1. Hồ Si Dam 2. Dang Đức Hanh Hà Nội - 2023 LỜI CAM ĐOAN Toi xin cam đoan luận án “Khung hình thức hỗ trợ đảm bao chất lượng chuyển đổi mô hình” là công trình nghiên cứu của riêng tôi. Các số liệu, kết quả được trình bày trong luận án là hoàn toàn trung thực và chưa từng được công bố trong bất kỳ một công trình nào khác.

m Toi đã trích dẫn day đủ các tài liệu tham khảo, công trình nghiên cứu liên quan ở trong nước và quốc tế. Ngoại trừ các tài liệu tham khảo này, luận án hoàn toàn là công việc của riêng tôi. » Trong các công trình khoa hoc được công bố trong luận án, tôi đã thể hiện rõ ràng và chính xác đóng góp của các đồng tác giả và những gì do tôi đã đóng góp. m Luận án được hoàn thành trong thời gian tôi làm Nghiên cứu sinh tại Bộ môn Công nghệ phần mềm, Khoa Công nghệ thông tin, Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội.

Tác giả: Hà Nội: LỜI CẢM ƠN Trước hết, tôi muốn bày tỏ sự biết ơn đến PGS. Hồ Sĩ Đàm và TS. Đặng Đức Hạnh, cán bộ hướng dẫn, các Thầy đã trực tiếp giảng day và định hướng tôi trong suốt thời gian thực hiện luận án. Một vinh dự lớn cho tôi được học tập, nghiên cứu cứu dưới sự hướng dẫn của các Thầy.

Tôi xin được bày tỏ sự biết ơn sâu sắc đến các Thay Cô trong Bộ môn Công nghệ phần mềm vì sự giúp đỡ của các Thầy Cô về các đóng góp rất hữu ích cho luận An. Tôi xin trân trọng cảm ơn Khoa Công nghệ thông tin, Phòng Đào tạo và Ban giám hiệu trường Đại học Công Nghệ đã tạo điều kiện thuận lợi cho tôi trong suốt quá trình thực hiện luận án. Tôi cũng bày tỏ sự biết ơn đến Trường Dai học Sư phạm Ha Nội đã tạo điều kiện về thời gian và tài chính cho tôi thực hiện luận án này. Tôi muốn cảm ơn đến Ban chủ nhiệm khoa, các cán bộ giảng viên Khoa Công nghệ thông tin - Trường Đại học Sư phạm Hà Nội đã cổ vũ, động viên và tạo điều kiện về thời gian cho tôi trong suốt quá trình nghiên cứu.

Tôi muốn cảm ơn đến tất cả những người bạn, các anh chị em nghiên cứu sinh và những người đồng nghiệp của tôi. Những người đã luôn chia sẻ với tôi những khó khăn và động viên giúp đỡ tôi bất cứ khi nào tôi cần và tôi luôn ghi nhớ điều đó. Cuối cùng, tôi xin bày tỏ lòng biết ơn vô hạn đối với cha mẹ, chồng, con và gia đình đã luôn ủng hộ và yêu thương tôi một cách vô điều kiện. Nếu không có sự ủng hộ của gia đình và chồng con tôi không thể hoàn thành được luận án nay.

Nguyễn Thị Hạnh ii ili TOM TAT Kỹ nghệ hướng mô hình (Model-Driven Engineering - MDE) dang trỏ thành một phương pháp phổ biến để phát triển các ứng dụng phần mềm quy mô lớn, phức tạp, trong đó các bộ chuyển đổi mô hình đóng vai trò then chốt để hiện thực hóa các tác vụ của quy trình phát triển. Nhằm giải quyết các thách thức trong việc đảm bảo chất lượng các bộ chuyển đổi mô hình, luận án đề xuất phát triển một khung hình thức hỗ trợ kiểm thử hướng đặc tả các bộ chuyển đổi mô hình. Các đóng góp chính của luận án như sau. Đề xuất ngôn ngữ TC4MT (Test Cases for Model Transformations - TC4MT) cho phép đặc tả mức cao các loại cam kết khác nhau của bộ chuyển đổi mô hình như cam kết kiểu, cam kết hành vi và cam kết thể thức chuyển.

Cam kết kiểu gồm siêu mô hình nguồn và siêu mô hình đích mô tả kiểu của dữ liệu được thao tác bởi chuyển đổi mô hình sẽ được đặc tả bởi các đồ thị kiểu. Cam kết hành vi đặt ra thêm các ràng buộc trên các mô hình đầu vào, đầu ra, quan hệ giữa chúng được đặc tả bởi các mẫu đồ thị biểu diễn các tập tiền điều kiện, hậu điều kiện và bất biến của bộ chuyển đổi mô hình. Cam kết thể thức diễn đạt sự thay đổi đồng bộ của các phần tử mô hình nguồn và mô hình đích tại mỗi bước chuyển và được diễn đạt bởi các luật chuyển tam đồ thị. Sử dụng đặc tả làm cơ sở kiểm thử, luận án đề xuất hai hướng tiếp cận chính để kiểm thử các bộ chuyển đổi mô hình: (1) Kết hợp phân vùng dựa trên cam kết kiểu và cam kết hành vi để thiết kế bộ ca kiểm thử kiểm chứng tính đúng đắn về ngữ pháp, tính bảo toàn thông tin và tính đầy đủ của bộ chuyển đổi mô hình; (2) Phân tích quan hệ phụ thuộc giữa các luật diễn đạt cam kết thể thức để thiết kế bộ ca kiểm thử, kiểm chứng một cách có hệ thống các tính chất của bộ chuyển đổi mô hình.

Để đánh giá hiệu quả của các phương pháp đề xuất, luận án cài đặt một số vi dụ chuyển đổi mô hình cùng các công cụ hỗ trợ. Tién hành phân tích kết quả kiểm thử trên các ví dụ chuyển, luận án thảo luận về tính ứng dụng của phương pháp kiểm thử đề xuất và đánh giá hiệu quả phát hiện lỗi của các tập ca kiểm thử được sinh ra từ các phương pháp đó. Từ khóa: Chuyển đổi mô hình, Kiểm thử chuyển đổi mô hình, Kiểm thử hướng đặc ta, Văn phạm tam đồ thị, TC4MT. Mục lục Lời cam đoan i Lời cảm ơn ii Tom tat iii Muc luc iv Danh mục các từ viết tat vii Danh mục các bảng viii Danh muc cac hinh vé ix Chương 1.

Mở đầu 1 11 Đặt vấn đề .2 Mục tiêu và phạm vi nghiên cứu.3 Nội dung và phương pháp nghiên cứu.4 Các đóng góp chính của luậnấn .5 Cấu trúc luận ấn. Kiến thức cơ sở và hiện trạng nghiên cứu 12 2.1 Phát triển bộ chuyển đổi mô hình .1 Giới thiệu chung về chuyển đổi mô hinh.2 Cài đặt bộ chuyển đổi mô hình.3 Dam bảo chất lượng bộ chuyển đổi mô hình .2 Ví dụ chuyển đổi từ biểu đồ lớp UML sang lược đồ cơ sở dữ liệu quan hệ. Kiểm thử bộ chuyển đổi môhình .4 Văn phạm tam đồ thị.1 Chuyển đổi đồthị .2 Giới thiệu về văn phạm tam dé thi. Chuyển đổi mô hình dựa trên văn phạm tam đồ thị.5 Tổng kết chương.

ee 37 Mục lục V Chương 3. Ngôn ngữ đặc tả các bộ chuyển đổi mô hình TC4MT 38 3.2 Các nghiên cứu liên quan .3 Ngôn ngữ đặc tả [C4MT.1 Cũ pháp trừu tuong. Ngữ nghĩa thực thi của đặc tả chuyển.4 Thực thi các cam kết của đặc tả chuyển đổi TCAMT .1 Phân tích và thẩm định tập yêu cầu.2 Biên dịch tiền điều kiện, hậu điều kiện va bat biến sang ngOnngtOCL .5 Kiểm thử bộ chuyển đổi mô hình theo hướng đặc ta.6 Đánh giá ngôn ngữ đặc tả IC4MT.7 Tổng kết chương. Ặ Q Q TQ TQ TQ va 74 Chương 4.

Phương pháp kiểm thử chuyển đổi mô hình dựa trên siêu mô hình và cam kết hành vi chuyển 75 JNN.2 Các nghiên cứu liên quan .3 Tổng quan về phương pháp đề xuất .4 Phân vùng trên siêu mô hình và cam kết hành vi chuyển.1 Phân vùng dựa trên siêu mô hình .2 Phân vùng dựa trên cam kết hành vi chuyén.5 Phương pháp kết hợp phân vùng để kiểm thử các bộ chuyển đổi mô hình.1 Kết hợp phân vùng sinh tập ca kiểm thử phủ định .2 Kết hợp phân vùng sinh tập ca kiểm thử khẳng dinh. 92 46 Tổng kết chương. Q Q Q TQ ST ng v. Phương pháp kiểm thử chuyển đổi mô hình dựa trên tập luật chuyển 99 5.2 Các nghiên cứu liên quan .3 Tổng quan về phương pháp đề xuất.4 Phân tích quan hệ phụ thuộc luật.5 Sinh mô hình kiểm thử dựa trên quan hệ phụ thuộc luật.6 Tổng kết chương.

Q Q TQ TQ TQ va 117 Chương 6. Thực nghiệm và đánh giá 119 6. en 119 Mục lục vì 6.2 Công cụ hỗ trợ.1 Đánh giá phương pháp tiếp cận kiểm thử.2 Dánh giá bộ ca kiểm thử sinh ra bằng phương phap phân tích đột biến .4 Tổng kết chương. ee 138 Chương 7.1 Các đóng góp của luậnấn.2 Hướng phát triển.

ee 141 DANH MỤC CÁC CÔNG TRÌNH KHOA HỌC 143 TÀI LIỆU THAM KHẢO 144 DANH MỤC CÁC TỪ VIET TAT Từ viết tắt Tiếng Anh Tiếng Việt EMF Eclipse Modeling Framework Khung mô hình hóa Eclipse MDE Model - Driven Engineering Kỹ nghệ hướng mô hình MT Model Transformation Chuyển đổi mô hình MOF Meta-Object Facility Phương tiện siêu mô hình M2M Model to Model Mô hình sang mô hình M2T Model to Text Mô hình sang văn bản NAC Negative Application Condi- Điều kiện áp dụng phủ định tions OMG Object Management Group Nhóm quản lý đối tượng OCL Object Constraint Language Ngôn ngữ ràng buộc đối tượng PIM Platform Independent Model Mô hình độc lập nền tảng PSM Platform Specific Model Mô hình chuyên biệt nền tang QVT Query-View-Transformation Truy vấn - Quan sát - Chuyển RTL Restricted Graph Transforma- Ngôn ngữ chuyển đổi đồ thị bị tion Language giới hạn TC4MT Test Cases for Model Transfor- Ca kiểm thử cho chuyển đổi mations mô hình TGG Triple Graph Grammar Văn phạm tam đồ thị UML Unified Modeling Language Ngôn ngữ mô hình hóa thống nhất USE UML-based Specification En- Môi trường đặc tả dựa trên vironment UML vil DANH MỤC CÁC BANG 2.1 Anh xa các khái niệm của siêu mô hình hóa sang các thuật ngữ đồ thị định kiểu .1 Phát hiện các cam kết dư thừa trong đặc tả.2 So sánh hình thức diễn đạt ngôn ngữ đặc tả TC4MT.3 So sánh năng lực diễn đạt của ngôn ngữ đặc tả TC4MT .1 Các giá trị đại diện cho bản số và phân vùng tương ứng.2 Mô tả các tiêu chí bao phủ trong chiến lược kiểm thử phủ định 91 5.1 Tập phần tử trong các thành phần cấu trúc của luật khai báo 107 5.2 Quan hệ phụ thuộc giữa các luật chuyển đổi tiến của đặc tả chuyển đổi mô hình CD2RDBM_.3 Tiêu chí kiểm thử và chuỗi luật chuyển đổi tiến .1 Các loại toán tử đột biến ngữ nghĩa của hệ thống chuyển đổi mô hình .2 Cài đặt kiểm tht.3 Các tập mô hình kiểm thử dựa trên phân tích siêu mô hình và cam kết ngữ nghĩa chuyển .