1. Họ và tên: 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:

Quyết định số 1257/QĐ-ĐT ngày 13/12/2018 của Hiệu trưởng Trường Đại học Công nghệ về việc gia hạn thời gian học tập cho nghiên cứu sinh K22 (đợt 1)

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 𝜄? (ààm kở?i ạ?o) àà �? (ààm chuể?n tạ?ng táái). Bế?n tể? ààyđượ?c ử? ụ?ng trong ộ?t thậ?t táán ọ?c quay lui óó tể? sinh áác gả?đị?nh ế?u ơon áác gả?đị?nhđượ?c sinh ở?i thậ?t táánđượ?cđề? xấ?t ở?i Chen àà ộ?ng ự?. áác gả?đị?nhđượ?c sinh ở?i thậ?t táánđề? xấ?t óó tể? gả?m ố? ầ?n ầ?n sinh ạ?i gả?đị?nh khi kể?m cứ?ng áác pầ?n ề?mđãã ị? thayđổ?i. Bế?n tể? tả? ờ?i áác truy ấ?n tàành vêên àà thậ?t táán quay luiđượ?c íích ợ?p àào pươong páápđề? xấ?tđể? gả?m ố? ầ?n gả?đị?nh ầ?n sinh ạ?i khi kể?m cứ?ng pầ?n ề?mđdang tế?n óóa. ộ?t ôông ụ? ỗ? tợ? ũungđããđượ?c ààiđặ?t àà tự?c nghệ?m ớ?i ộ?t ố? ệ? tố?ng pổ? bế?n trong ộ?ngđồ?ng nghêên ứ?u àà cho nữ?ng ế?t qả? kả? quan.

Lậ?náán tự?c nghệ?m ààiđặ?t phêên ả?n ộ?t pha cho pươong pááp kể?m cứ?ng gả?đị?nh -đả?m ả?o hai phađượ?cđề? xấ?t ở?i Lin àà ộ?ng ự? cho pầ?n ề?m ự?a têên tàành pầ?n óó ààng bộ?c tờ?i gian. Phêên ả?n àày lạ?i ỏ? pha sinh gả?đị?nh kôông óó tờ?i gian ừ? qáá tìình kể?m cứ?ng. Lậ?náán ũung tìình àày ộ?t ố? ấ?nđề? páát sinh àà pươong pááp ử? ýý trong qáá tìình ààiđặ?t pươong pááp kể?m cứ?ng trong tự?c ế?. íínhđúúngđắ?n ủ?a phêên ả?nđề? xấ?tđượ?c tìình àày àà tả?o lậ?n trong lậ?náán. ôông ụ? ỗ? tợ?đããđượ?c ààiđặ?t àà tự?c nghệ?m ớ?i ộ?t ố? ệ? tố?ng pổ? bế?n trong ộ?ngđồ?ng nghêên ứ?u àà cho áác ế?t qả? kả? quan.

12. Kả? ăangứ?ng ụ?ng trong tự?c tễ?n: (ế?u óó)

13. Nữ?ng ướ?ng nghêên ứ?u tế?p theo: (ế?u óó)           

14. áác ôông tììnhđãã ôông ố? óó lêên quanđế?n lậ?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.