Thông tin luận án tiến sĩ của NCS Trần Hoàng Việt
Tên đề tài luận án: Một số cải tiến phương pháp kiểm chứng giả định – đảm bảo cho phần mềm dựa trên thành phần
1. Họ và tên nghiên cứu sinh: Trần Hoàng Việt . 2. Giới tính: Nam
3. Ngày sinh: 15/05/1982 4. Nơi sinh: Vĩnh Phúc
5. Quyết định công nhận nghiên cứu sinh số: 640/QĐ-CTSV, ngày 03 tháng 09 năm 2015 của Hiệu trưởng Trường Đại Học Công Nghệ.
6. Các thay đổi trong quá trình đào tạo: Không
7. Tên đề tài luận án: Một số cải tiến phương pháp kiểm chứng giả định – đảm bảo cho phần mềm dựa trên thành phần
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. Phạm Ngọc Hùng
TS. Võ Đình Hiếu
11. Tóm tắt các kết quả mới của luận án:
Đề xuất một phương pháp sinh các giả định nhỏ nhất và mạnh nhất cục bộ để giảm chi phí của bài toán kiểm chứng giả định – đảm bảo. Ý tưởng chính của phương pháp đề xuất là tích hợp một biến thể của kỹ thuật trả lời các câu truy vấn thành viên vào trong thuật toán học đề xuất được cải tiến từ thuật toán của Cobleigh. Ngoài ra, phương pháp này cũng sử dụng các ứng viên cho giả định được sinh bởi thuật toán của Cobleigh làm cơ sở để phân tích. Với một ứng viên cơ sở này, để có giả định nhỏ nhất, luận án kiểm tra các ứng viên cho giả định nhỏ nhất Ai với kích thước tăng dần. Việc này được tiến hành bằng cách lấy tổ hợp chập t của các trạng thái từ tập trạng thái của Ai, với 1 < t < |Ai|. Trong các ứng viên cho giả định nhỏ nhất có cùng kích thước t, với mỗi ứng viên C (|L(C)| = n), phương pháp này kiểm tra mọi khả năng từ khả năng chỉ có một chuỗi đến khả năng có n-1 chuỗi thuộc vào L(C). Phương pháp này dừng ngay khi tìm được giả định đầu tiên thỏa mãn luật kiểm chứng giả định – đảm bảo. Do đó, giả định được sinh bởi phương pháp được đề xuất là giả định nhỏ nhất và mạnh nhất cục bộ. Một công cụ hỗ trợ cũng đã được cài đặt và thực nghiệm với một số ví dụ điển hình để minh chứng cho tính hiệu quả của phương pháp đề xuất.
Đề xuất một phương pháp kiểm chứng hồi quy giả định – đảm bảo một cách hiệu quả cho phần mềm tiến hóa. Để làm việc này, luận án đề xuất một biến thể của kỹ thuật trả lời các truy vấn thành viên cho hai thực thể thuật toán học CDNF 𝜄 (hàm khởi tạo) và 𝜏 (hàm chuyển trạng thái). Biến thể này được sử dụng trong một thuật toán học quay lui có thể sinh các giả định yếu hơn các giả định được sinh bởi thuật toán được đề xuất bởi Chen và cộng sự. Các giả định được sinh bởi thuật toán đề xuất có thể giảm số lần cần sinh lại giả định khi kiểm chứng các phần mềm đã bị thay đổi. Biến thể trả lời các truy vấn thành viên và thuật toán quay lui được tích hợp vào phương pháp đề xuất để giảm số lần giả định cần sinh lại khi kiểm chứng phần mềm đang tiến hóa. Một công cụ hỗ trợ cũng đã được cài đặt và thực nghiệm với một số hệ thống phổ biến trong cộng đồng nghiên cứu và cho những kết quả khả quan.
Đề xuất ba cải tiến cho phương pháp kiểm chứng giả định – đảm bảo cho hệ thống phần mềm có ràng buộc thời gian. Đầu tiên, luận án loại bỏ pha học không có thời gian khỏi quá trình học làm giảm độ phức tạp về thời gian của quá trình học. Thứ hai, luận án đề xuất dùng một giá trị maxbound trong thuật toán trả lời các truy vấn ứng viên được cài đặt trong Teacher. Giá trị này đóng vai trò như một chỉ báo để Teacher trả về kết quả “không biết” cho Learner để ngăn không cho quá trình học bị lặp vô hạn. Cuối cùng, luận án đề xuất một phương pháp phân tích phản ví dụ nhận được từ Teacher và một phương pháp tiền xử lý các phản ví dụ trước khi được trả về cho Learner. Sự kết hợp của hai phương pháp này giúp quá trình kiểm chứng không bị lặp vô hạn trong nhiều trường hợp và tiến gần hơn đến kết quả có thể kết luận được trong quá trình học. Luận án cũng đã cài đặt một công cụ và tiến hành thực nghiệm với một số hệ thống phổ biến và cho kết quả tốt.
12. Khả năng ứng dụng trong thực tiễn:
13. Những hướng nghiên cứu tiếp theo:
14. Các công trình đã công bố có liên quan đến luận án:
- Hoang-Viet Tran, Pham Ngoc Hung, Viet-Ha Nguyen, Toshiaki Aoki (2020). A Framework For Assume-Guarantee Regression Verification Of Evolving Software, Science of Computer Programming, ISSN 0167-6423. https://doi.org/10.1016/j.scico.2020.102439. (ISI Indexed).
- Hoang-Viet Tran, Quang-Trung Nguyen, and Pham Ngoc Hung (2019). On Implementation of the Improved Assume-Guarantee Verification Method for Timed Systems. In Soict ’19: The Tenth International Symposium on Information and Communication Technology, December 4-6, 2019, Hanoi – Ha Long Bay, Vietnam. ACM, New York, NY, USA, 8 pages. https://doi.org/10.1145/3368926.3369659, pp. 457-464.
- Hoang-Viet TRAN, Ngoc Hung PHAM, Viet Ha NGUYEN (2019). ON LOCALLY MINIMUM AND STRONGEST ASSUMPTION GENERATION METHOD FOR COMPONENT-BASED SOFTWARE VERIFICATION, IEICE Transactions on Information and Systems. ISSN 0916-8532, Vol.E102-D, No.8, pp.1449-1461. (ISI Indexed).
- Hoang-Viet Tran and Ngoc Hung PHAM (2018). On Locally Strongest Assumption Generation Method for Component-Based Software Verification. VNU Journal of Science: Computer Science and Communication Engineering, vol. 34, no. 2, pp. 16_32. ISSN 2588-1086.
- Hoang-Viet Tran, Ngoc Hung PHAM, Dang Van Hung (2018). On Improvement of Assume-Guarantee Verification Method for Timed Component-Based Software. 10th International Conference on Knowledge and Systems Engineering (KSE), Ho Chi Minh City, pp. 270-275.
- Chi-Luan Le, Hoang-Viet Tran, and Pham Ngoc Hung (2017). On Implementation of the Assumption Generation Method for Component-Based Software Verification. Advanced Topics in Intelligent Information and Database Systems. Springer International Publishing, pp. 549-558.
- Chi-Luan Le, Hoang-Viet Tran, Pham Ngoc Hung (2016), A Framework for Modeling and Modular Verifying of Component-based System Designs, VNU Journal of Science: Computer Science and Communication Engineering, vol. 32, no. 2, pp. 31-42.
- Hoang-Viet Tran, Chi-Luan Le and Ngoc Hung Pham (2016), A Strongest Assumption Generation Method for Component-Based Software Verification, In Addendum Proc. of the 2016 IEEE-RIVF International Conference on Computing and Communication Technologies, pp. 1-6.
