1. Họ và tên nghiên cứu sinh: Lê Hồng Anh
2. Giới tính: Nam
3. Ngày sinh: 17/10/1980
4. Nơi sinh: Vĩnh Phúc
5. Quyết định công nhận nghiên cứu sinh số: 3205/QĐ-ĐT ngày 08 tháng 11 năm 2010.
6. Các thay đổi trong quá trình đào tạo:
Thay đổi tên đề tài luận án tiến sĩ theo quyết định số 34/QĐ-ĐT, ngày 18/01/2013. Tên đề tài: Phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện
7. Tên đề tài luận án: Phương pháp mô hình hóa và kiểm chứng các hệ thống hướng sự kiện
8. Chuyên ngành: Kỹ thuật phần mềm
9. Mã số: 62.48.01.03
10. Cán bộ hướng dẫn khoa học: PGS.TS Trương Ninh Thuận, PGS.TS Phạm Bảo Sơn
11. Tóm tắt các kết quả mới của luận án:
1. Luận án đề xuất một phương pháp mô hình hóa và kiểm chứng các hệ thống CSDL có sử dụng triggers. Quá trình chuyển đổi dựa trên sự tương đồng giữa cơ chế hoạt động của trigger và sự kiện Event-B. Với phương pháp này, các thuộc tính bảo toàn ràng buộc dữ liệu có thể được kiểm chứng, đồng thời có thể phát hiện các vòng lặp vô hạn bằng các chứng minh hình thức. Phương pháp này làm giảm chi phí phát triển ứng dụng vì có thể phát hiện ra lỗi từ khâu thiết kế và dễ ứng dụng trong phá triển phần mềm. Một công cụ hỗ trợ mô hình hóa tự động cũng đã được phát triển.
2. Luận án tiếp tục nghiên cứu các lợi ích của sự tương đồng giữa các luật ECA và sự kiện Event-B, từ đó đề xuất một phương pháp mô hình hóa và kiểm chứng các hệ thống cảm ngữ cảnh. Luận án cũng ứng dụng các lợi thế của cơ chế làm mịn Event-B để mô hình hóa từng bước. Các tính chất quan trọng như bảo toàn ràng buộc ngữ cảnh được xác định như các bất biến và được kiểm chứng tự động với công cụ Rodin
3. Luận án nghiên cứu các hệ thống hướng sự kiện được mô tả bởi các yêu cầu không chính xác. Các yêu cầu này có thể được biểu diễn bởi các luật If-Then mờ. Luận án đề xuất phương pháp biểu diễn các yêu cầu này bằng lý thuyết tâp hợp, sau đó đề xuất các tập luật đề biến đổi thành các thành phần Event-B. Chúng tôi cũng mở rộng mô hình hóa các hệ thống thời gian bằng việc đưa ra khái niệm tập luật mờ thời gian If-Then
4. Luận án ứng dụng cơ chế làm mịn của Event-B và phương pháp biểu diễn các khái niệm mờ để phân tích các tính chất quan trọng của các yêu cầu không chính xác của hệ thống như tính an toàn (safety) và kết quả hoạt động (eventuality).
12. Khả năng ứng dụng trong thực tiễn:
13. Những hướng nghiên cứu tiếp theo:
Nghiên cứu phát triển các phương pháp dựa trên Event-B để mô hình hóa và kiểm chứng các thuộc tính có ràng buộc về thời gian. Nghiên cứu xây dựng thêm các công cụ hỗ trợ mô hình hóa tự động.
14. Các công trình đã công bố có liên quan đến luận án:
1) Hong Anh Le and Ninh Thuan Truong. Modeling and Verifying WS-CDL Using Event- B. In Proc. ICCASA 2012. LNICST Vol 109, pp. 290-299, Springer, 2013.
2) Hong Anh Le and Ninh Thuan Truong: Modeling and Verifying DML Triggers Using Event-B, In Proc. ACIIDS 2013. LNCS Vol 7083, Vol 2, pp. 539-548, Spinger, 2013.
3) Hong Anh Le, Loan Dinh Thi and Ninh Thuan Truong: Modeling and Verifying Im- precise Requirements of Systems Using Event-B. In Proc. KSE 2013. AISC Vol 244, pp. 313-325, Springer, 2013.
4) Hong Anh Le and Ninh Thuan Truong: Formal Modeling and Verification of Context-Aware Systems Using Event-B. In Proc. ICCASA 2013. LNICST Vol 128, pp. 250-259, Springer 2014 (The best paper award).
5) Hong Anh Le and Ninh Thuan Truong: Formal Modeling and Verification of Context-Aware Systems Using Event-B. In EAI Endorsed Transactions on Context-Aware Systems and Applications, Vol 2, e4, 2014. ISSN 2409-0026.
6) Hong Anh Le, Ninh Thuan Truong and Shin Nakajima: Verifying Eventuality Properties of Imprecise System Requirements. The 30th ACM/SIGAPP Symposium On Applied Computing - Software Engineering Track, April 13–17, 2015. Salamanca, Spain.
>>>> Xem thông tin bản tiếng Anh.
