1. Full name: Trần Hoàng Việt                                       2. Sex: Male     

3. Date of birth: 15 May 1982                                        4. Place of  birth: Vĩnh Phúc     

5. Admission decision number: 640/QĐ-CTSV… Dated: 03 Sep 2015      

6. Changes in academic process:

Decision number 1257/QĐ-ĐT dated 13/12/2018 of the Rector of VNU University of Engineering and Technology about extending the study period for graduate students K22 (1st phase)

7. Official thesis title: On Improvements of Assume-Guarantee Verification Method for Component-Based Software         

8. Major: Software Engineering  9. Code: 9480103.01    

10. Supervisors: Assoc. Prof. Dr. Phạm Ngọc Hùng

                           Dr. Võ Đình Hiếu       

11. Summary of the new findings of the thesis:

Propose a method to generate minimum and strongest assumptions to reduce the cost of assume-guarantee verification. The key idea of the method is to integrate a variant of the membership queries answering algorithm of Cobleigh into an algorithm to generate the minimum and strongest assumptions. In addition, the method also use assumption candidates generated from Cobleigh’s algorithm as a basis for analysis. For each of these candidates, to get the minimum assumptions, the dissertation checks all candidates Ai with ascending size. This is done by getting the t-combinations of states of Ai, with 1 < t < |Ai|. Among those assumption candidates with minimum size of t, for each candidate C (|L(C)| = n), the method checks every ability from one trace to n-1 traces belong to L(C). This method stops right after reaching the first assumption which satisfies the assume-guarantee rule. As a result, the generated assumptions are locally minimum and strongest. An implemented tool is presented to perform experiment with some common systems in the research community to show the effectiveness and efficiency of the proposed method.

Propose a method to do regression assume-guarantee verification of component-based software effectively in the software evolution context. For this purpose, this dissertation proposes a variant of the membership queries answering algorithm for the two instances CDNF 𝜄? (initial function) and ���? (transition function). This variant is used in the proposed backtracking algorithm to generate locally weakest assumptions. These assumptions can reduce the number of assumption regeneration times when rechecking evolving software. This variant algorithm and backtracking algorithm are integrated into a method to verify evolving software to reduce the assumption regeneration times. An implemented to is used to perform experiment to evaluate the usefulness and effectiveness of the proposed algorithms and method with potential results.

Present the result of the implementation and experiment process of the one-phase version of the two-phase assume–– guarantee verification method for timed systems. This process is to give evaluation of time cost and effectiveness of the one-phase verification process. Two problems during the implementation process and corresponding solutions are also presented. The first one is when Teacher does not know if continuing the verification process can generate the required assumption or Teacher does not know what counterexample to return to Learner for it to generate a better assumption candidate. The second one is to realize the idea to find an appropriate counterexample to return to Learner of Teacher and to analyze the received counterexample in Learner to generate a better assumption candidate. The correctness of the proposed methods is presented and discussed. An implemented tool is shown and used to perform experiments with some common systems with potential results.

12. Practical applicability, if any:           

13. Further research directions, if any:   

14. Thesis-related publications:

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.