1. Họ và tên nghiên cứu sinh: Đỗ Văn Chiểu

2. Giới tính: Nam

3. Ngày sinh: 19/08/1979

4. Nơi sinh: Hải Phòng

5. Quyết định công nhận nghiên cứu sinh số: 4154/QĐ-SĐH ngày 15 tháng 07 năm 2008 của Giám đốc Đại học Quốc gia Hà Nội.

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ố 201 /QĐ-ĐT,  ngày 09 tháng 04 năm 2011. Tên đề tài: Mô hình hóa và đặc tả hình thức các giao diện thành phần có chứa chất lượng dịch vụ và tính tương tranh

7. Tên đề tài luận án: Mô hình hóa và đặc tả hình thức các giao diện thành phần có chứa chất lượng dịch vụ và tính tương tranh.

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: TS. Đặng Văn Hưng; PGS.TS. Nguyễn Việt Hà

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

Luận án đề xuất lý thuyết Vết thời gian để hỗ trợ đặc tả các ràng buộc về thời gian trên các hệ thống tương tranh có ràng buộc thời gian. Vết thời gian là một sự mở rộng về thời gian của Vết Mazurkiewicz bằng việc bổ sung vào Vết Mazurkiewicz một hàm gán nhãn thời gian. Với việc mở rộng này, Vết thời gian có thể dễ dàng đặc tả các hành vi của hệ thống tương tranh có ràng buộc thời gian. Trong lý thuyết này, luận án còn đề xuất khái niệm Vết khoảng. Vết khoảng là các Vết Mazurkiewicz mà mỗi ký hiệu (hành động) trong bảng chữ cái phụ thuộc được gán một ràng buộc là một khoảng thời gian. Vết khoảng được sử dụng để biểu diễn các ràng buộc thời gian của các hệ thống mà mỗi hành động của các hệ thống này có ràng buộc về khoảng thời gian hoạt động và cung cấp dịch vụ. Vết khoảng là biểu diễn ngắn gọn của một tập các Vết thời gian. Luận án cũng đưa vào ô-tô-mát khoảng bất đồng bộ làm công cụ đoán nhận lớp ngôn ngữ Vết thời gian chính quy để sử dụng trong các bài toán về kiểm chứng hệ thống. Luận án chứng minh rằng bài toán kiểm tra tính rỗng của ô-tô-mát khoảng bất đồng bộ là quyết định được dù độ phức tạp không phải là đa thức. Để hỗ trợ việc biểu diễn đặc tả các thuộc tính cần kiểm chứng của các hệ thống, luận án đưa vào lôgic thời gian thực tuyến tính đặc tả thuộc tính của các Vết thời gian. Lôgic này là một mở rộng về thời gian của lôgic thời gian tuyến tính (LTL - Linear Temporal Logic). Mối quan hệ giữa ô-tô-mát khoảng bất đồng bộ và  lôgic này cũng được đề cập và chứng minh. Như vậy, với lý thuyết Vết thời gian đề xuất, các hệ thống tương tranh có ràng buộc thời gian sẽ dễ dàng được đặc tả và kiểm chứng bằng các ô-tô-mát khoảng bất đồng bộ và các công thức của lôgic thời gian thực tuyến tính.

Để minh chứng cho tính hiệu quả của phương pháp được đề xuất, luận án áp dụng phương pháp này vào việc đặc tả, phân tích và kiểm chứng cho ba mô hình ứng dụng thiết kế hệ thống dựa trên thành phần. Với mỗi mô hình, các hành vi của hệ thống được đặc tả thông qua các Vết thời gian. Như vậy, các mô hình này có thể đặc tả được các tính chất tương tranh và ràng buộc về thời gian của các hệ thống cần kiểm chứng, cụ thể:

- Thứ nhất, luận án giới thiệu một mô hình hệ thống tương tranh thời gian dựa trên lý thuyết rCOS (Refinement of Component and Object Systems). Nghiên cứu này sử dụng Vết thời gian trong đặc tả các thể thức giao diện thành phần. Các tính toán về phép ghép nối, phương pháp làm mịn thành phần được đưa ra và chứng minh.

-  Thứ hai, luận án đề xuất một mô hình thiết kế dựa trên giao diện cho các hệ tương tranh. Trong mô hình này, luận án sử dụng ô-tô-mát giao diện tương tranh thời gian để đặc tả mỗi thành phần. Các kết quả trong nghiên cứu đã chỉ ra rằng phương pháp mới đảm bảo tất cả các yêu cầu của lý thuyết thiết kế dựa trên giao diện.

-  Thứ ba, luận án giới thiệu một phương pháp là một mô hình hỗ trợ đặc tả và kiểm chứng cho hệ thống phân tán. Ý tưởng của phương pháp là mở rộng hệ dịch chuyển phân tán, sử dụng Vết thời gian để đặc tả ngôn ngữ và chỉ ra ra mối quan hệ tương đương giữa Vết thời gian và hệ dịch chuyển phân tán tương đương về ngôn ngữ.

12. Khả năng ứng dụng trong thực tiễn: Kết quả trong luận án có thể ứng dụng vào trong các kỹ thuật mô hình giao diện trong lý thuyết về giao diện cho các hệ thống dựa trên thành phần có ràng buộc về thời gian và tính tương tranh.

13. Những hướng nghiên cứu tiếp theo: Áp dụng lý thuyết nghiên cứu cho một công cụ kiểm chứng mô hình cụ thể, nghiên cứu và tối ưu độ phức tạp của các thuật toán kiểm chứng trong luận án.

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

[1]  Do Van Chieu and Dang Van Hung (2010), An extension of Mazurkiewicz traces and their applications in specication of real-time systems, In Proceedings of the second international Conference on knowledge and systems engineering 2010. IEEE Computer Society, pp. 167-172.

[2] Do Van Chieu and Dang Van Hung (2011), A formal model for concurrent real-time component-based systems, Tạp chí Khoa học và Công nghệ - Viện Khoa học và Công nghệ Việt Nam, Vol. 49, No.4A, pp. 313-226 (ISSN: 0866 708X).

[3] Do Van Chieu and Dang Van Hung (2012), Timed traces and their applications in specication and veriction of distributed real-time systems, In Proceedings of the Third International Symposium on Information and Communication Tecnology 2012, IEEE Computer Society, pp. 31-41.

[4] Do Van Chieu (2015), A Formal Method for Specifying Interface of Component in Real-time Concurrent Systems, Tạp chí Bưu chính Viễn thông, Vol. E-3, No. 8(12), pp. 48-57 (ISSN: 1859 – 3534).

>>> Tải về bản tóm tắt luận án tiếng Việt, tiếng Anh