1. Họ và tên: Nguyễn Thị Hạnh                                       2. Giới tính: Nữ

3. Ngày sinh: 12/12/1986                                                4. Nơi sinh: Hà Nội

5. Quyết định công nhận nghiên cứu sinh số 654/QĐ-CTSV ngày 05/09/2016 của Hiệu trưởng Trường Đại học công nghệ, Đại học Quốc gia Hà Nội.

6. Các thay đổi trong quá trình đào tạo:

Gia hạn thời gian học tập theo Quyết định số 1127/QĐ-ĐT ngày 17 tháng 10 năm 2019 của Hiệu trưởng Trường Đại học Công nghệ.

7. Tên đề tài luận án: Khung hình thức hỗ trợ đảm bảo chất lượng chuyển đổi mô hình.

8. Chuyên ngành: Kỹ thuật phần mềm                            9. Mã số: 9480103.01

10. Cán bộ hướng dẫn khoa học: PGS.TS. Hồ Sĩ Đàm; TS. Đặng Đức Hạnh

11. Tóm tắt các kết quả mới của luận án

Luận án đã đề xuất được một khung kiểm thử hướng đặc tả để đảm bảo chất lượng chuyển đổi mô hình với các đóng góp chính như sau.

Thứ nhất, luận án đề xuất được một ngôn ngữ đặc tả chuyển đổi mô hình dựa trên cam kết có tên TC4MT (Test Cases for Model Transformations). Ngôn ngữ TC4MT cho phép đặc tả tập yêu cầu chính thức của các bộ chuyển đổi mô hình dựa trên tập cam kết ở nhiều mức độ khác nhau. Ngôn ngữ TC4MT được thiết kế dựa trên cú pháp biểu diễn và ngữ nghĩa nghĩa hình thức chuyển đổi đồ thị. Các cam kết trong đặc tả chuyển được biểu diễn dưới dạng các mẫu đồ thị thuộc tính hóa định kiểu có cấu trúc tương tự sơ đồ lớp UML trực quan và dễ sử dụng. Các luật chuyển đổi mô hình của đặc tả TC4MT được thiết kế dựa trên các luật viết lại đồ thị của văn phạm tam đồ thị (Triple Graph Grammars) không chỉ giúp biểu diễn các đặc trưng phức tạp của chuyển đổi mô hình (ví dụ như chuyển đổi hai chiều, chuyển đổi có hỗ trợ truy vết mô hình, chuyển đổi với các luật xóa), mà còn hỗ trợ phân tích các điều kiện kiểm thử ở mức độ đặc tả một cách có hệ thống nhằm kiểm chứng các thuộc tính chất lượng của cài đặt chuyển.

Thứ hai, luận án đề xuất phương pháp kết hợp phân vùng trên siêu mô hình diễn đạt cam kết mức kiểu và các cam kết hành vi để sinh tập mô hình kiểm thử hộp đen theo hai chiến lược kiểm thử khẳng định và kiểm thử phủ định. Đồng thời đề xuất phương pháp cấu trúc các phán xét kiểm thử kiểm chứng tính đúng đắn về ngữ pháp, tính đầy đủ và tính bảo toàn thông tin tĩnh của các bộ chuyển đổi mô hình trong các chiến lược kiểm thử khác nhau.

Thứ ba, luân án đề xuất phương pháp kiểm thử các bộ chuyển đổi mô hình dựa trên phân tích tập cam kết thể thức chuyển được biểu diễn bởi các luật chuyển. Phương pháp đề xuất phân tích quan hệ phụ thuộc giữa các luật chuyển mức đặc tả để thiết kế các ca kiểm thử dựa trên cách tiếp cận kiểm thử văn phạm. Phân tích các thuộc tính chất lượng dựa trên ngữ nghĩa trên văn phạm tam đồ thị, luận án đề xuất việc kết hợp tập ca kiểm thử được sinh ra từ quan hệ phụ thuộc luật với việc chỉ định các hàm phán xét kiểm thử tương ứng.

Bên cạnh đó, luận án cài đặt được công cụ hỗ trợ và tiến hành các thực nghiệm để đánh giá phương pháp đề xuất. Luận án tiến hành thực nghiệm kiểm thử trên một số ví dụ chuyển đổi mô hình để chỉ ra tính ứng dụng của phương pháp đề xuất và hiệu quả của bộ ca kiểm thử được tạo ra sử dụng kỹ thuật phân tích điểm đột biến.

12. Khả năng ứng dụng trong thực tiễn

Kỹ nghệ hướng mô hình (Model-Driven Engineering - MDE) đang trở thành một phương pháp kỹ thuật phổ biến để phát triển các ứng dụng phần mềm quy mô lớn. Các bộ chuyển đổi mô hình là nguyên tắc kỹ nghệ chính để hiện thực hóa quy trình phát triển phần mềm. Kiểm thử để đảm bảo chất lượng của các bộ chuyển đổi mô hình là nhu cầu tất yếu đặt ra để hiện thực hóa thành công MDE trong công nghiệp. Phương pháp đề xuất bởi luận án có khả năng áp dụng trên mô hình ở nhiều mức độ trừu tượng khác nhau (mô hình độc lập tính toán, mô hình độc lập nền tảng và mô hình phụ thuộc nền tảng), với điều kiện siêu mô hình định nghĩa các loại mô hình này được biểu diễn dựa trên chuẩn phương tiện siêu mô hình (Meta Object Facility - MOF).

13. Những hướng nghiên cứu tiếp theo:

Phát triển ngôn ngữ TC4MT để cho phép đặc tả các hành vi cập nhật giá trị thuộc tính bên trong phần tử của các mô hình vào và ra để đặc tả các kịch bản đồng bộ hóa mô hình tự động.

Cài đặt các chuyển đổi mô hình ở mức cao (HOT: Higher Order Transformations) để cho phép sinh tự động cài đặt chuyển đổi mô hình từ đặc tả chuyển diễn đạt bởi ngôn ngữ TC4MT.

Bổ sung thêm các cài đặt và thực nghiệm kiểm thử hướng đặc tả TC4MT để kiểm chứng tính bảo toàn hành vi động, tính hội tụ và tính kết thúc của các ứng dụng chuyển đổi mô hình trong công nghiệp.

14. Các công trình đã công bố có liên quan đến luận án:

Thi-Hanh Nguyen, and Duc-Hanh Dang (2018). An approach for testing model transformations. In Proc. of the 10th International Conference on Knowledge and Systems Engineering, IEEE Xplore pp.264-269. (DBLP)

Thi-Hanh Nguyen, Duc-Hanh Dang, and Quang-Trung Nguyen (2019). On Analyzing Rule-Dependencies to Generate Test Cases for Model Transformations. In Proc. of the 11th International Conference on Knowledge and Systems Engineering, IEEE Xplore pp.181-186. (DBLP)

Thi-Hanh Nguyen, Duc-Hanh Dang (2021). A Graph Analysis Based Approach for Specification-Driven Testing of Model Transformations. In Proc. Of the 8th NAFOSTED Conference on Information and Computer Science, IEEE Xplore pp.224-230.

Thi-Hanh Nguyen, Duc-Hanh Dang. On integrating multiple restriction domains to automatically generate test cases of model transformations. Informatica - An International Journal of Computing and Informatic (Accepted).

Thi-Hanh Nguyen, Duc-Hanh Dang. A Contract-Based Specification Method for Model Transformations. Submitted to VNU Journal of Science: Computer Science and Communication Engineering (Accept with revisions).

Thi-Hanh Nguyen, Duc-Hanh Dang. TC4MT: A SpecificationDriven Testing Framework for Model Transformations. Submitted to International Journal of Software Engineering and Knowledge Engineering.