1. Họ và tên nghiên cứu sinh: Nguyễn Trịnh Đông                      

2. Giới tính: Nam                                                                      

3. Ngày sinh: 12/07/1974                                                           

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

5. Quyết định công nhận nghiên cứu sinh: Số 3613/QĐ-SĐH  ngày 22/10/2009 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:

7. Tên đề tài luận án: Một số phương pháp mô hình hoá và kiểm chứng hình thức cho các hệ thống thời gian thực hướng thành phầ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:              TS. Đặng Văn Hưng; PGS.TS. Trương Anh Hoàng

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

Thứ nhất, luận án đã đề xuất mở rộng mô hình PECOS (PErvasive COmponent Systems) cho thành phần phần mềm thời gian thực với mục đích tạo ra một mô hình thành phần phần mềm có thể phân tích nhiều yếu tố khác nhau từ chức năng đến phi chức năng. Mô hình này được chia thành hai phần, phần thụ động và phần chủ động. Phần thụ động đóng vai trò như một kho chứa các thành phần phần mềm thời gian thực có khả năng đáp ứng mọi yêu cầu của thiết kế. Phần chủ động đóng vai trò tương tác với môi trường, nhận các yêu cầu từ môi trường và gọi các dịch vụ từ phần thụ động để xử lý, sau đó lấy kết quả trả về cho môi trường.  Ngoài chức năng trên, mô hình được chia thành hai phần cũng nhằm mục đích giảm độ phức tạp, do cách phát triển dựa trên chiến lược chia để trị và kiểm soát được các tiến trình song song, trong những hệ thống phát triển dựa trên mô hình này. Mô hình này cũng cho phép các tiến trình của các thành phần phần mềm ở cả hai phần thực hiện thực hiện song song. Bên cạnh đó, để phân tích chính xác sự tương tác trong hệ thống thời gian thực dựa trên thành phần, luận án đề xuất thể thức tương tác tương tranh thời gian và thể thức tương tranh có ràng buộc tài nguyên bằng cách tiến hành đặc tả thứ tự lời gọi các dịch vụ trong thành phần phần mềm bằng biểu thức chính quy thời gian trên bảng chữ cái phân tán và mô hình hóa các dãy hành vi của môi trường hệ thống bằng ôtômát thời gian và ôtômát trọng số. Đồng thời, luận án cũng đề xuất thuật toán kiểm tra sự tuân thủ của dãy hành vi của môi trường với thể thức của thành phần phần mềm trên khía cạnh chức năng và phi chức năng. Sự tuân thủ thể thức tương tác còn cho biết khả năng sử dụng hiệu quả các tài nguyên mà môi trường dành cho các thành phần phần mềm.

Thứ hai, luận án mở rộng lý thuyết giao diện thành phần trở thành lý thuyết giao diện thời gian thực để đặc tả và mô hình hóa các hệ thống thời gian thực dựa trên thành phần. Giao diện thời gian thực là một bộ ba thành phần gồm tập biến đầu vào, tập biến đầu ra và mối quan hệ giữa tập biến đầu vào và tập biến đầu ra và thời gian ràng buộc trên mối quan hệ này. Mối quan hệ này được biểu diễn bằng biểu thức lôgíc tân từ cấp 1 nhằm khẳng định rằng nếu môi trường gán một bộ giá trị thỏa điều kiện trên tập biến đầu vào của giao diện thì giao diện sẽ đảm bảo dữ liệu đầu ra sẽ thỏa yêu cầu của môi trường hệ thống trong một khoảng thời gian theo thiết kế. Với cách tiếp cận này, một thành phần phần mềm được đặc tả đơn giản hơn, cô đọng hơn nhưng lại phản ánh được chi tiết các hành vi và chức năng của thành phần phần mềm. Do các hành vi của giao diện thành phần thời gian thực là vô hạn nên luận án sử dụng ôtômát khoảng (duration automata) để biểu diễn hữu hạn các dãy hành vi của giao diện thành phần và môi trường thời gian thực. Ôtômát khoảng có ưu điểm là có thể mô hình hóa và biểu điễn được khoảng thời gian lớn nhất và nhỏ nhất dành cho một hành vi trong thành phần phần mềm. Việc sử dụng giao diện thời gian thực với quan hệ trên tập biến đầu vào/đầu ra có thể đặc tả và kiểm chứng hệ thống thời gian thực dựa trên thành phần một cách hiệu quả. 

Thứ ba, luận án đề xuất kỹ thuật đặc tả thành phần phần mềm bằng hợp đồng thời gian và hợp đồng thời gian với các ràng buộc tài nguyên dựa trên cách tiếp cận tính đúng đắn bởi cách xây dựng và thiết kế bằng hợp đồng. Kỹ thuật này cho phép đặc tả thành phần phần mềm thời gian thực chi tiết đến từng phương thức và tập biến đầu vào đầu ra của phương thức cũng như ràng buộc trên tập biến đầu vào/đầu ra. Bên cạnh đó, phương pháp đặc tả này cũng chỉ rõ thành phần phần mềm cần những phương thức và loại tài nguyên nào để có thể thực thi được yêu cầu của hệ thống và cung cấp những dịch vụ gì cho môi trường với các chi phí tài nguyên là bao nhiêu. Phương pháp này cũng cho phép đặc tả các thành phần bất biến, thành phần bất biến tài nguyên, đặc tả các phương thức. Đặc biệt, phương pháp này cũng đặc tả thể thức tương tác của các dịch vụ trong thành phần phần mềm và môi trường sử dụng chúng. Cụ thể, trong một thành phần phần mềm, trình tự thực thi của các phương thức được biểu diễn bằng biểu thức chính quy thời gian thực có ràng buộc tài nguyên. Khi môi trường muốn sử dụng các dịch vụ từ thành phần phần mềm thì môi trường phải cung cấp đủ tài nguyên cho các dịch vụ và môi trường phải tuân thủ thứ tự lời gọi các dịch vụ trong thành phần phần mềm. Nhờ sự tuân thủ này, thành phần phần mềm sẽ đảm bảo được chất lượng của các dịch vụ mà nó cung cấp. Do đó, bằng kỹ thuật này, một hệ thống thời gian thực dựa trên thành phần được phát triển tăng dần dựa trên việc ghép các hợp đồng thời gian thực và các yếu tố được phân tích và đánh giá đầy đủ trên hai khía cạnh chức năng và phi chức năng. Để có thể triển khai trên thực tế, luận án cũng đề xuất ngôn ngữ đặc tả thời gian thực mẫu nhằm hợp nhất các ngôn ngữ đặc tả thời gian thực với đầy đủ tính năng đặc tả về phần chức năng và phi chức năng cho thành phần phần mềm. Dựa trên kỹ thuật này, các thành phần phần mềm thời gian thực được đặc tả đầy đủ và các đặc tả được sử dụng làm cơ sở cho cho việc nâng cao chất lượng phần mềm.

12. Khả năng ứng dụng trong thực tiễn:

- Các kết quả chính trong luận án có thể ứng dụng cho phát triển hệ thống thời gian thực hướng thành phần có quy mô lớn và độ phức tạp cao.

13. Những hướng nghiên cứu tiếp theo:  Dưới đây luận án tóm tắt một số vấn đề có thể nghiên cứu trong tương lai.

Luận án đang nghiên cứu mở rộng mô hình thời gian thực cho hệ thống có quy mô lớn trên thực tế như hệ thống nhúng, rô bốt, hệ thống tác tử di động và triển khai cho các dịch vụ web trên cơ sở các thể thức tương tác tương tranh thời gian có ràng buộc tài nguyên. Phát triển bộ công cụ phát triển phần mềm cho hệ thống thời gian thực dựa trên lý thuyết đã đề xuất.

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

[1]  Nguyen Trinh Dong, Dang Van Hung and Truong Anh Hoang (2011), “Real-Time Relational Interface Behavior Modeling and Specification”, KSE 2011-Third International Conference on Knowledge and Systems Engineering, pages 112-119.

[2]   Nguyen Trinh Dong (2015), “Memory Resource Estimation of Component-Based Systems”, 4th International Conference, ICCASA 2015, Vung Tau, Vietnam, November 26-27, pages 73-82.

[3]   Dang Van Hung, Nguyen Trinh Dong and Truong Anh Hoang (2017), "A Model for Real-timed Concurrent Interaction Protocols in Component Interfaces", VNU Journal of Science: Computer Science and Communication Engineering, vol.33, no.1, pages 8-15.

[4]   Nguyen Trinh Dong, Dang Van Hung, Truong Anh Hoang (2017), “A formal contract-based model for component-based real-time systems”, The 4^th National Foundation for Science and Technology Development Conference on Information and Computer Science (NICS 2017), pages 230-235.

[5]  Nguyen Trinh Dong (2017), “A General Model for Quality Analyzing of Functional and Non-functional Features in Real-Time Systems”, The 6^th Conference on Information Technology and Its application (CITA 2017), pages 15-22.