Tiến Sĩ 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 tr

Tóm tắt

Chất lượng dịch vụ của một hệ thống bao gồm thời gian tiến hành, tài nguyên tiêu thụ và độ tin cậy của dịch vụ, trong đó thì chất lượng dịch vụ về thời gian đang được quan tâm nhiều, thể hiện rằng thời gian cung ứng dịch vụ tốt hơn. Ràng buộc thời gian trong các hệ thống thường được phân chia thành hai loại là ràng buộc thời gian cứng (hard) và mềm (soft). Luận án quan tâm tới các ràng buộc thời gian cứng. Để chất lượng dịch vụ tốt, các phương thức trong hệ thống cần được tiến hành song song (tăng tốc độ đáp ứng) nếu có thể và phải có ràng buộc thời gian rõ ràng. Ràng buộc thời gian thể hiện thời gian tối thiểu và tối đa mà phương thức cần để có thể cung cấp dịch vụ, tức là không được gọi phương thức quá “dày”, nếu không có thể sẽ gây ra tình trạng dịch vụ không đáp ứng được. Luận án quan tâm tới phương pháp đặc tả hệ thống có chứa chất lượng dịch vụ về thời gian.

Đối tượng nghiên cứu của luận án là các hệ thống phần mềm dựa trên thành phần có tính tương tranh và có ràng buộc về thời gian. Tính tương tranh là một thuộc tính của hệ thống trong đó một số dịch vụ của hệ thống được cho phép truy cập một cách song song. Ràng buộc về thời gian trong luận án là các yêu cầu về thời gian thực thi của các hành động trong hệ thống, mỗi hành động sẽ được gắn với một khoảng thời gian cho việc thực thi của nó. 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 về 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.

Các kết quả của luận án đạt được như sau. 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 thời gian thực. 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 và Vết thời gian có mối quan hệ với nhau, 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. Một kết quả trong luận án là 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, trong lý thuyết Vết thời gian, 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ấ đồ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. 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ữ.

Các kết quả trong luận án đã được công bố qua các công trình đã được xuất bản và có đóng góp phần nào vào việc nghiên cứu, đặc tả và kiểm chứng các hệ thống có tính tương tranh và ràng buộc về thời gian.

Mục lục
1 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 . 8
2 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 . 50
3 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
i
4 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 . 81
5 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 . 96
6 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 . 110
7 Kết luận 112
7.1 Các kết quả đạt được 112
7.2 Hướng phát triển tiếp theo . 114