Luận án Tiến sĩ Công nghệ thông tin: 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

Mục đích của luận án là phát triển một phương pháp hình thức để đặc tả và kiểm chứng các giao diện của các thành phần phần mềm có tính tương tranh và ràng buộc thời gian. Sau đó luận án áp dụng phương pháp được đề xuất vào việc đặc tả, phân tích và kiểm chứng các mô hình khác nhau của các hệ thống phần mềm dựa trên thành phần. Mời các bạn cùng tham khảo nội dung chi tiết.
Nội dung trích xuất từ tài liệu:
Luận án Tiến sĩ Công nghệ thông tin: 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 tranhMục lục1 Giới thiệu 1 1.1 Đặt vấn đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Các kết quả chính của luận án . . . . . . . . . . . . . . . . . . . . . 5 1.3 Bố cục của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 Kiến thức nền tảng 10 2.1 Công nghệ phần mềm dựa trên thành phần . . . . . . . . . . . . . 11 2.1.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.1.2 Các công nghệ xây dựng hệ thống phần mềm dựa trên thành phần hiện nay . . . . . . . . . . . . . . . . . . . . . . 13 2.1.3 Đảm bảo chất lượng cho các hệ thống phần mềm dựa trên thành phần . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2 Ô-tô-mát thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.2.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.2.2 Ô-tô-mát thời gian . . . . . . . . . . . . . . . . . . . . . . . 21 2.2.3 Công cụ UPPAAL . . . . . . . . . . . . . . . . . . . . . . . 29 2.3 Lý thuyết Vết và ứng dụng trong đặc tả hệ thống tương tranh . . 36 2.3.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.3.2 Vết Mazurkiewicz . . . . . . . . . . . . . . . . . . . . . . . . 37 2.3.3 Ô-tô-mát đoán nhận ngôn ngữ Vết . . . . . . . . . . . . . . 43 2.3.4 Logic trên Vết . . . . . . . . . . . . . . . . . . . . . . . . . . 46 2.4 Kết luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 503 Lý thuyết Vết thời gian 51 3.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 3.2 Vết thời gian và ô-tô-mát khoảng bất đồng bộ . . . . . . . . . . . 53 3.2.1 Vết thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 3.2.2 Ô-tô-mát khoảng bất đồng bộ . . . . . . . . . . . . . . . . . 57 3.3 Lôgic trên Vết thời gian . . . . . . . . . . . . . . . . . . . . . . . . 61 3.4 Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . 65 3.5 Kết luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 i4 Một mô hình cho hệ thống tương tranh có ràng buộc thời gian dựa trên các khái niệm và kỹ thuật rCOS 67 4.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.2 Kiến trúc thành phần và các giao thức tương tác . . . . . . . . . . 69 4.3 Vết thời gian và biểu diễn của nó . . . . . . . . . . . . . . . . . . . 70 4.4 Mô hình thành phần . . . . . . . . . . . . . . . . . . . . . . . . . . 71 4.4.1 Thiết kế . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4.4.2 Giao diện và hợp đồng . . . . . . . . . . . . . . . . . . . . . 73 4.4.3 Ghép nối các hợp đồng . . . . . . . . . . . . . . . . . . . . . 75 4.4.4 Thành phần . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.5 Kết luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 815 Phương pháp đặc tả các thành phần trong hệ tương tranh có ràng buộc thời gian theo nguyên lý thiết kế dựa trên giao diện 83 5.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 5.2 Ô-tô-mát giao diện tương tranh có ràng buộc thời gian . . . . . . 85 5.2.1 Định nghĩa . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 5.2.2 Khả năng ghép nối và Tích song song các TCIA . . . . . . 88 5.2.3 Làm mịn các thành phần . . . . . . . . . . . . . . . . . . . 92 5.3 Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . 94 5.4 Kết luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 966 Mô hình đặc tả và kiểm chứng các hệ phân tán có ràng buộc thời gian dựa trên hệ dịch chuyển phân tán 98 6.1 Hệ phân tán có ràng buộc thời gian . . . . . . . . . . . . . . . . . . 99 6.2 Lôgic thời gian trên cấu hình Foata . . . . . . . . . . . . . . . . . . 103 6.3 Bài toán kiểm chứng . . . . . . . . . . . . . . . . . . . . . . . . . . 108 6.4 Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . 109 6.5 Kết luận . . . . . . . . . . . . . . . . . . . ...