Luận án 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 tranh

Mục lục 1 Giới thiệu 1 1.2 Các kết quả chính của luận án .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 .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 .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 .2 Ô-tô-mát thời gian .2 Ô-tô-mát thời gian .3 Công cụ UPPAAL .3 Lý thuyết Vết và ứng dụng trong đặc tả hệ thống tương tranh .3 Ô-tô-mát đoán nhận ngôn ngữ Vết .4 Logic trên Vết. 50 3 Lý thuyết Vết thời gian 51 3.2 Vết thời gian và ô-tô-mát khoảng bất đồng bộ .1 Vết thời gian .2 Ô-tô-mát khoảng bất đồng bộ .3 Lôgic trên Vết thời gian .4 Các nghiên cứu liên quan. 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.2 Kiến trúc thành phần và các giao thức tương tác .3 Vết thời gian và biểu diễn của nó .4 Mô hình thành phần .2 Giao diện và hợp đồng .3 Ghép nối các hợp đồng.

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.2 Ô-tô-mát giao diện tương tranh có ràng buộc thời gian .2 Khả năng ghép nối và Tích song song các TCIA .3 Làm mịn các thành phần .3 Các nghiên cứu liên quan. 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 .2 Lôgic thời gian trên cấu hình Foata .3 Bài toán kiểm chứng .4 Các nghiên cứu liên quan .1 Các kết quả đạt được .2 Hướng phát triển tiếp theo. 114 ii Danh sách hình vẽ 1.1 Cấu trúc luận án .1 Mô hình phát triển CBSE .2 Kiến trúc CBSE .3 Đồng hồ là một hàm thời gian .4 Mô hình điều khiển đèn không có thời gian .5 Mô hình điều khiển đèn có thời gian .6 Mô hình hệ thống điều khiển thanh chắn tàu .7 Thuộc tính Safety và Real-time Liveness của bài toán mô hình hệ điều khiển đóng mở thanh chắn tàu .8 Mạng các ô-tô-mát thời gian .9 Ô-tô-mát tích của hai ô-tô-mát trong Hình 2.10 Ví dụ một mạng với các vùng thời gian không lồi .11 Kiến trúc hệ thống của UPPAAL .12 Đồ thị phụ thuộc của bảng chữ cái phụ thuộc .13 Một đồ thị biểu diễn của Vết Mazurkiewicz .14 Ánh xạ wtot() cho từ abcba .15 Một ô-tô-mát bất đồng bộ .16 Ý nghĩa của Until .1 Sơ đồ thứ tự bộ phận Vết thời gian được cho trong ví dụ 3.2 Sơ đồ thứ tự bộ phận của một Vết khoảng được cho trong ví dụ 3.3 Sơ đồ thứ tự bộ phận của Vết khoảng (T, J) và và Vết thời gian (T 0 , θ) thỏa (T, J) .4 Một ADA với hàm gán thời gian J trong ví dụ 3.5 Ngữ nghĩa của toán tử EXI .6 Ngữ nghĩa của toán tử UI .1 Kiến trúc hệ thống .2 Thời gian và thứ tự của M code(m) và phép chiếu của nó trên các phương thức của B .1 Một TCIA P với JP (a) = [1, 2], JP (b) = [2, 3], JP (c) = [1, 3] (i) và đồ thị chuyển trạng thái tương ứng (ii) .2 TCIA Q với JQ (b) = [2, 3], JQ (c) = [1, 3], JQ (d) = [2, 4] (i) và đồ thị chuyển trạng thái tương ứng (ii) là tương thích với TCIA P trong Ví dụ 5.3 Kết quả phép tích song song giữa P và Q trong Hình 5.1 Hệ phân tán có yếu tố thời gian và các thực thi đồng bộ và bất đồng bộ của nó .2 Một Vết thời gian .3 Cấu hình Foata của một Vết thời gian trong Hình 6.4 Đồ thị cấu hình Foata của Vết thời gian được chỉ ra trong Hình 6.2105 iv Danh sách bảng 2.1 Bảng so sánh giữa các công nghệ .2 Bảng chuyển của ô-tô-mát bất đồng bộ của Hình 2.1 Bảng chuyển của TCIA P trong ví dụ 5.2 Bảng chuyển của TCIA Q trong ví dụ 5. 89 v Bảng các từ viết tắt Từ viết tắt Từ gốc Giải nghĩa-Tạm dịch AA Asynchronous Automata Ô-tô-mát bất đồng bộ ADA Asynchronous Duration Au- Ô-tô-mát khoảng bất tomata đồng bộ CBSE Component-based Software Công nghệ phần mềm dựa Enginnering trên thành phần CBSD Component-based Software Phát triển phần mềm dựa Development trên thành phần DTS Distributed Transition Sys- Hệ dịch chuyển phân tán tems DDTS Duration Distributed Transi- Hệ dịch chuyển phân tán tion Systems khoảng TCIA Timed Concurrent Interface Ô-tô-mát giao diện tương Automata tranh thời gian UTP Unifying Theories of Program- Lý thuyết hợp nhất về lập ming trình (tạm dịch) TA Timed Automata Ô-tô-mát thời gian LTL Linear Temporal Logic Logic thời gian tuyến tính TLTL Timed Linear Temporal Logic Logic thời gian tuyến tính có ràng buộc thời gian rCOS Refinement of Component and Làm mịn thành phần và Object Systems các hệ thống đối tượng COM Component Object Model Mô hình đối tượng thành phần DCOM Distributed Component Ob- Mô hình đối tượng thành ject Model phần phần tán CORBA Common Object Request Bro- ker Architecture ORB Object Request Broker OMG Object Management Group Tập đoàn quản lý đối tượng COTS Component Off The Shelf Thành phần thương mại có sẵn TW Timed Word Từ thời gian vi Từ viết tắt Từ gốc Giải nghĩa-Tạm dịch RTS Real-time systems Các hệ thời gian thực CCS Calculus of Communicating Tính toán các hệ thống Systems giao tiếp CTL Computational Tree Logic Logic cây tính toán TCTL Timed Computational Tree Logic cây tính toán có Logic thời gian P roc Process Ký hiệu tiến trình wtot word to trace Ký hiệu hàm chuyển từ "từ" sang "Vết" ttow trace to word Ký hiệu hàm chuyển từ "Vết" sang "từ" BA Büchi Automata Ô-tô-mát Bu-khi conf Configuration Ký hiệu cấu hình CG Configuration Graph Ký hiệu đồ thị cấu hình WCET Worst-case Execution Time Thời gian thực thi yếu nhất dtot duration to timed Ký hiệu hàm chuyển thời khoảng sang thời điểm tT rL timed Trace Language Ngôn ngữ Vết thời gian intv inteval Ký hiệu khoảng thời gian pref prefix Ký hiệu tiền tố P roj Project Ký hiệu phép chiếu dur duration Ký hiệu khoảng Ctr Contract Hợp đồng Comp Component Thành phần Behav Behavior Hành vi ActComp Active Component Thành phần chủ động SysCtr System Contract Hợp đồng hệ thống vii Lời cam đoan Tôi xin cam đoan đây là công trình nghiên cứu do tôi thực hiện dưới sự hướng dẫn của TS.

Đặng Văn Hưng và PGS. Nguyễn Việt Hà tại bộ môn Công nghệ Phần mềm, Khoa Công nghệ Thông tin, Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội. Các số liệu và kết quả trình bày trong luận án là trung thực, chưa được công bố bởi bất kỳ tác giả nào hay ở bất kỳ công trình nào khác. Tác giả viii Lời cảm ơn Luận án này được thực hiện tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội dưới sự hướng dẫn khoa học của TS Đặng Văn Hưng và PGS.

Nguyễn Việt Hà. Nghiên cứu sinh xin bày tỏ lòng biết ơn sâu sắc tới các Thầy về định hướng khoa học, sự quan tâm, hướng dẫn và các chỉ bảo kịp thời cho các hướng nghiên cứu, tạo điều kiện thuận lợi trong suốt quá trình nghiên cứu tại trường. Nghiên cứu sinh cũng xin cảm ơn tới các thày cô trong Bộ môn Công nghệ Phần mềm. Trong quá trình thực hiện luận án, nghiên cứu sinh đã nhận được sự giúp đỡ nhiệt tình và sự động viên kịp thời của các thầy cô, các nhà khoa học.

Đây là nguồn động lực lớn để tôi có thể hoàn thành luận án. Nghiên cứu sinh xin trân trọng cảm ơn Lãnh đạo Trường Đại học Công nghệ, Đại học Quốc Gia Hà Nội đã tạo những điều kiện tốt nhất để nghiên cứu sinh có được môi trường nghiên cứu tốt nhất và hoàn thành chương trình nghiên cứu của mình. Xin chân thành cám ơn Khoa Công nghệ Thông tin, Phòng Đào tạo và đào tạo sau đại học và các nhà khoa học thuộc trường Đại học Công nghệ cũng như các nghiên cứu sinh khác về sự hỗ trợ trên phương diện hành chính, hợp tác có hiệu quả trong suốt quá trình nghiên cứu khoa học của mình. Nghiên cứu sinh xin gửi lời cảm ơn tới Ban Lãnh đạo Trường Đại học Dân lập Hải Phòng, Khoa Công nghệ Thông tin và các bạn đồng nghiệp vì đã tạo nhiều điều kiện thuận lợi hỗ trợ cho nghiên cứu sinh có thời gian và toàn tâm thực hiện triển khai đề tài nghiên cứu của luận án.

Nghiên cứu sinh cũng xin trân trọng cảm ơn các nhà khoa học, tác giả các công trình công bố đã trích dẫn trong luận án vì đã cung cấp nguồn tư liệu quý báu, những kiến thức liên quan trong quá trình nghiên cứu hoàn thành luận án. Cuối cùng là sự biết ơn tới Bố Mẹ, vợ con, các anh chị em trong gia đình và những người bạn thân thiết đã liên tục động viên để duy trì nghị lực, sự cảm thông, chia sẻ về thời gian, sức khỏe và các khía cạnh của cuộc sống trong cả quá trình hoàn thành luận án. ix 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” 1 , 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ó.