Luận án trình bày nội dung tóm tắt các nghiên cứu nền tảng cho các nghiên cứu tiếp theo của luận án, đưa ra lý thuyết vết thời gian dựa trên vết Mazurkiewicz, trình bày một ứng dụng của lý thuyết vết trong việc mô hình hóa hệ thống tương tranh thời gian thực dựa trên việc sử dụng vết thời gian cho đặc tả các thể thức giao diện thành phần được mở rộng từ lý thuyết rCOS,. Để biết rõ hơn về nội dung chi tiết, . | ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ĐỖ VĂN CHIỂU 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 LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN Hà Nội – 2014 Công trình được hoàn thành tại khoa Công nghệ Thông tin, Trường Đại học Công nghệ , Đại học Quốc Gia Hà Nội. Người hướng dẫn khoa học: TS. Đặng Văn Hưng . Nguyễn Việt Hà Phản biện 1: Phản biện 2: Phản biện 3: Có thể tìm hiểu luận án tại: - Thư viện Quốc gia Việt Nam - Trung tâm Thông tin – Thư viện, Đại học Quốc gia Hà Nội Chương 1 Giới thiệu Giới thiệu Trong luận án này, chúng tôi tập trung nghiên cứu đề xuất phương pháp hình thức hỗ trợ mô hình hóa và đặc tả các giao diện thành phần có chứa các ràng buộc thời gian và tính tương tranh và xây dựng ứng dụng. Ý tưởng cơ bản của phương pháp đề xuất trong luận án là mở rộng về thời gian trên vết Marzukiewicz. Kết quả của mở rộng này là đưa ra lý thuyết về vết thời gian, ô-tô-mát đoán nhận ngôn ngữ vết và logic đặc tả thuộc tính vết cũng như mối quan hệ giữa chúng. Để chứng minh tính hiệu quả của phương pháp đề xuất, chúng tôi áp dụng lý thuyết này mở rộng một số mô hình thiết kế hệ thống hướng thành phần để hỗ trợ đặc tả các thuộc tính tương tranh có các ràng buộc thời gian. Thứ nhất, chúng tôi đề xuất một phương pháp hình thức cho đặc tả các hệ thống tương tranh thời gian thực hướng thành phần dựa trên mô hình của lý thuyết rCOS. Thứ hai, luận án đề xuất mở rộng mô hình thiết kế dựa trên giao diện cho các hệ tương tranh có ràng buộc thời gian bằng các ô-tô-mát giao diện tương tranh thời gian. Thứ ba, luận án đã xây dựng một ứng dụng của vết thời gian hỗ trợ đặc tả và kiểm chứng cho một hệ thống phân tán. Các kết quả trong luận án đã được minh chứng qua các công trình đã được xuất bản và có ý nghĩa lớn trong việc nghiên cứu, sử dụng để đặc tả các hệ có ràng buộc thời gian và tương tranh. Bố cục của luận án Dựa trên các mục tiêu và đối tượng nghiên cứu,
