Mô Hình Hóa và Kiểm Chứng Hệ Thống Thời Gian Thực: Nghiên Cứu và Ứng Dụng

Luận án tiến sĩ nghiên cứu 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át triển phương pháp mới, đánh giá hiệu quả ứng

• Tác giả: Nguyễn Trịnh Đông
• Người hướng dẫn: TS. Đặng Văn Hưng
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Kỹ thuật phần mềm
• Đề tài: Phương Pháp Mô Hình Hóa và Kiểm Chứng Hệ Thống Thời Gian Thực
• Loại tài liệu: Luận án tiến sĩ
• Năm xuất bản: 2018
• Địa điểm: Hà Nội

Tóm tắt

I. Tổng Quan Về Mô Hình Hóa Hệ Thống Thời Gian Thực 55 ký tự

Phát triển phần mềm thời gian thực dựa trên thành phần đóng vai trò quan trọng trong lĩnh vực công nghệ phần mềm. Các hệ thống phần mềm được phát triển bằng cách ghép dần các thành phần cho đến khi thỏa các yêu cầu của hệ thống. Dựa trên cách tiếp cận này, hệ thống được phát triển một cách nhanh chóng, dễ bảo trì và độ chính xác cao. Tuy nhiên, một trong những hạn chế lớn nhất của phương pháp này là làm thế nào đảm bảo được tính đúng đắn của hệ thống sau khi ghép các thành phần phần mềm. Đặc biệt, đối với các hệ thống thuộc lĩnh vực hàng không, vũ trụ, tự động hóa, an ninh quốc phòng, v.v. Hiện nay, các lý thuyết và kỹ thuật phát triển phần mềm dựa trên thành phần đang ở mức kiểm tra hệ thống phần mềm từ giai đoạn triển khai, trong khi đó việc đảm bảo tính đúng đắn của hệ thống cần phải được giải quyết ngay tại giai đoạn thiết kế.

1.1. Lịch Sử Phát Triển Mô Hình Hóa Thời Gian Thực

Hiện nay, kiểm chứng mô hình và chứng minh định lý đang được xem là hai cách tiếp cận chính để giải quyết những hạn chế trên. Đối với phương pháp kiểm chứng mô hình, người ta sử dụng ôtômát thời gian để biểu diễn các chuỗi hành vi hệ thống. Tuy nhiên, do tập trạng thái của ôtômát thời gian là vô hạn nên người ta sử dụng ôtômát vùng (regional automata) để biểu diễn hữu hạn ôtômát thời gian. Trong phương pháp này, các tính chất của hệ thống cần kiểm chứng được biểu diễn bằng một trong các loại lôgíc như lôgíc thời gian tuyến tính (LTL - Linear temporal logic), lôgíc cây tính toán (CTL - Computation tree logic), v.v.

1.2. Ưu Điểm và Hạn Chế Của Phương Pháp Mô Hình Hóa

Phương pháp kiểm chứng này thường được thực hiện tại giai đoạn triển khai và đôi khi mã nguồn chương trình được sử dụng như là một mô hình của hệ thống để đưa vào kiểm chứng. Tuy nhiên, đối với những hệ thống quy mô lớn nếu áp dụng phương pháp kiểm chứng mô hình sẽ dẫn đến độ phức tạp cao, bùng nổ không gian trạng thái, chi phí lớn và còn nhiều nguy cơ tiềm ẩn. Ngoài những lý do trên, việc ghép các thành phần phần mềm thời gian thực cũng làm cho bài toán kiểm chứng mô hình đối diện với hiện tượng bùng nổ không gian trạng thái.

II. Thách Thức Trong Kiểm Chứng Hệ Thống Thời Gian Thực 60 ký tự

Đặc biệt, các ràng buộc thời gian trên các chuỗi hành vi trong hệ thống thời gian thực cũng làm tăng khó khăn trong việc kiểm chứng dựa trên mô hình. Bên cạnh yếu tố thời gian, các ràng buộc tài nguyên như hiệu năng CPU, năng lượng, băng thông mạng, bộ nhớ, dung lượng thiết bị lưu trữ, v.v. cũng tạo ra thách thức rất lớn trong quá trình kiểm chứng hệ thống thời gian thực dựa trên thành phần có tính toán đến các yếu tố tài nguyên. Đối với phương pháp kiểm chứng phần mềm dựa trên chứng minh định lý, tính đúng đắn của phần mềm được chứng minh và kiểm tra dựa trên các biểu thức toán học và cũng chỉ tập trung vào những hệ thống phi thời gian.

2.1. Vấn Đề Bùng Nổ Trạng Thái Khi Kiểm Chứng

Một trong những thách thức lớn nhất là việc đảm bảo tính đúng đắn của hệ thống sau khi ghép các thành phần phần mềm. Việc ghép các thành phần phần mềm thời gian thực cũng làm cho bài toán kiểm chứng mô hình đối diện với hiện tượng bùng nổ không gian trạng thái.

2.2. Ràng Buộc Thời Gian và Tài Nguyên trong Hệ Thống

Luận án xác định bài toán đặc tả các yếu tố chức năng và phi chức năng làm một trong những bài toán quan trọng cần phải giải quyết. Hơn nữa, bài toán kiểm chứng hệ thống thời gian thực với các ràng buộc chức năng và phi chức năng thường đối diện với việc bùng nổ không gian trạng thái, độ phức tạp cao. Vì vậy, luận án áp dụng lý thuyết giao diện thời gian thực, thiết kế bằng hợp đồng và tính đúng đắn dựa trên cách xây dựng để giải quyết bài toán đặc tả và kiểm chứng hệ thống thời gian thực.

2.3. Đảm bảo Độ Tin Cậy Hệ Thống Thời Gian Thực

Mục đích của luận án là đề xuất các kỹ thuật đặc tả và kiểm chứng hình thức hệ thống thời gian thực dựa trên thành phần một cách hiệu quả. Trong đó, luận án cần phải xác định rõ mô hình thành phần phần mềm của hệ thống cần kiểm chứng nhằm đề xuất những kỹ thuật kiểm chứng phù hợp.

III. Phương Pháp Mô Hình Hóa và Kiểm Chứng Hiệu Quả 59 ký tự

Luận án bắt đầu bằng việc đề xuất mô hình cho thành phần phần mềm thời gian thực. Mô hình này được phát triển theo chiến lược chia để trị nhằm phát huy các ưu điểm của phương pháp phát triển phần mềm thời gian thực dựa trên thành phần và cho phép phát triển hệ thống có quy mô tăng dần dựa trên việc ghép các thành phần phần mềm. Luận án cũng bổ sung thể thức tương tác thời gian thực vào đặc tả thành phần phần mềm để kiểm soát sự tương tác giữa các thành phần phần mềm và giữa các thành phần phần mềm với môi trường để hệ thống hoạt động hiệu quả trên cả khía cạnh thực thi và khía cạnh duy trì các hoạt động.

3.1. Ứng Dụng Lý Thuyết Giao Diện Thời Gian Thực

Để 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.

3.2. Thiết Kế Bằng Hợp Đồng để Kiểm Chứng

Phương pháp kiểm chứng này thường được thực hiện tại giai đoạn triển khai và đôi khi mã nguồn chương trình được sử dụng như là một mô hình của hệ thống để đưa vào kiểm chứng. Tuy nhiên, đối với những hệ thống quy mô lớn nếu áp dụng phương pháp kiểm chứng mô hình sẽ dẫn đến độ phức tạp cao, bùng nổ không gian trạng thái, chi phí lớn và còn nhiều nguy cơ tiềm ẩn.

IV. Đề Xuất Mô Hình PECOS cho Hệ Thống Thời Gian Thực 59 ký tự

Thứ nhất, luận án đề xuất mô hình thành phần phần mềm gian thực dựa trên sự mở rộng mô hình PECOS cho hệ thống thời gian thực. Mô hình có hai phần, phần thụ động và phần chủ động. Phần thụ động đóng vai trò làm một kho lưu trữ, tập hợp các thành phần phần mềm đủ lớn để đáp ứng tất cả các yêu cầu của hệ thống. 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 sau đó gọi các dịch vụ từ phần thụ động để thực hiện rồi trả kết quả lại môi trường.

4.1. Kiến Trúc Hệ Thống Theo Mô Hình PECOS

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 cho đến khi thỏa mọi yêu cầu của hệ thống. 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.

4.2. Thể Thức Tương Tác và Ràng Buộc Tài Nguyên

Ngoài ý nghĩa 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 của hệ thống do cách phát triển dựa trên chiến lược chia để trị. Trong đó, với phần chủ động, chúng ta có thể 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; phần thụ động đóng vai trò làm một kho chứa các thành phần phần mềm, chúng ta phát triển hệ thống thời gian thực bằng cách ghép các thành phần phần mềm trong phần này cho đến khi thỏa yêu cầu của hệ thống.

V. Đặc Tả Thành Phần Bằng Giao Diện Thời Gian Thực 57 ký tự

Thứ hai, luận án đề xuất phương pháp đặc tả và mô hình hóa thành phần bằng lý thuyết giao diện thời gian với quan hệ đầu vào/đầu ra và biểu diễn hữu hạn giao diện thời gian thực bằng ôtômát khoảng. Dựa trên sự đặc tả và mô hình hóa này, các giao diện...

5.1. Biểu Diễn Hữu Hạn Bằng Ôtômát Khoảng

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ách hành vi và chức năng của thành phần phần mềm. Do cách 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.

5.2. Quá Trình Kiểm Chứng Tăng Dần

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ả. Sự kiểm chứng được thực thực hiện bằng quá trình phát triển tăng dần từng bước dựa trên các phép ghép, phép làm mịn và phép cắm môi trường vào thành phần phần mềm.

VI. Hợp Đồng Thời Gian và Ràng Buộc Tài Nguyên 55 ký tự

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.

6.1. Đảm Bảo Chất Lượng Dịch Vụ

Đặ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.

6.2. Phát Triển Tăng Dần Dựa Trên Hợp Đồng

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.

Trích đoạn nội dung tài liệu

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nguyễn Trịnh Đông MỘT SỐ PHƯƠNG PHÁP MÔ HÌNH HÓA 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 LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN Hà Nội - 2018 TIEU LUAN MOI download : [e-mail] ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nguyễn Trịnh Đông MỘT SỐ PHƯƠNG PHÁP MÔ HÌNH HÓA 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 Chuyên ngành: Kĩ thuật Phần mềm Mã số: 9480103.01 LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: 1. Trương Anh Hoàng Hà Nội - 2018 TIEU LUAN MOI download : [e-mail] Mục lục Trang Mục lục . i Danh mục hình vẽ . v Danh mục bảng . vii Phụ lục . xv Chương 1. Các đóng góp chính của luận án . Bố cục của luận án . Kiến thức nền tảng . Phát triển phần mềm dựa trên thành phần . Kỹ nghệ phần mềm dựa trên thành phần. Tính đúng đắn bởi cách xây dựng . Kiến trúc hệ thống phát triển phần mềm dựa trên thành phần . Các phương pháp mô hình hóa hệ thống thời gian thực. Ôtômát thời gian và vùng thời gian . Ôtômát trọng số . 19 i TIEU LUAN MOI download : skknchat@gmail. Bài toán kiểm chứng hệ thống thời gian thực . Đặc tả và mô hình hóa hệ thống . Đặc tả tính chất của hệ thống . Bài toán kiểm tra tính rỗng . Tổng kết chương . Mô hình thành phần phần mềm thời gian thực và thể thức tương tác . Các nghiên cứu liên quan . Mô hình thành phần phần mềm thời gian thực . Mô hình thành phần phần mềm . So sánh các mô hình thành phần phần mềm . Thể thức tương tác tương tranh ràng buộc thời gian . Thể thức tương tác . Thuật toán kiểm chứng tính cắm được . Thể thức tương tác thời gian thực ràng buộc tài nguyên . Thể thức thời gian - tài nguyên . Mô hình hóa và sự tuân thủ thể thức thời gian - tài nguyên . Tổng kết chương . Đặc tả và mô hình hóa giao diện thời gian thực . Các nghiên cứu liên quan . 70 ii TIEU LUAN MOI download : skknchat@gmail. Giao diện thành phần phần mềm thời gian thực . Ghép giao diện thành phần . Sự làm mịn giao diện thành phần . Mô hình hóa hành vi của giao diện . Tổng kết chương . Đặc tả và kiểm chứng bằng hợp đồng thời gian thực với ràng buộc tài nguyên . Các nghiên cứu liên quan . Hợp đồng thời gian . Thiết kế thời gian . Ghép hợp đồng . Hợp đồng thời gian-tài nguyên . Thiết kế thời gian - tài nguyên . Hợp đồng thời gian - tài nguyên . Hệ thống thời gian - tài nguyên . Ngôn ngữ đặc tả thời gian thực mẫu . Tổng kết chương . Các kết quả đạt được . Hướng phát triển tiếp theo . 132 Danh mục công trình nghiên cứu của tác giả liên quan đế luận án. 134 iii TIEU LUAN MOI download : [e-mail] Tài liệu tham khảo . 135 iv TIEU LUAN MOI download : [e-mail] Danh mục hình vẽ 1.1 Các đóng góp chính của luận án.1 Minh họa giao diện thành phần phần mềm.2 Minh họa phép ghép song song (a) và phép ghép nối tiếp (b).3 Minh họa kiến trúc chung hệ thống CB-RTS.4 Minh họa máy bán hàng bằng ôtômát hữu hạn.5 Minh họa phép giao hai khoảng (a) và phép ghép nối tiếp hai khoảng (b).1 Minh họa mô hình thành phần phần mềm.2 Minh họa hệ thống điều tiết không khí và nhiệt độ.3 Minh họa chuỗi hành động ω trên trục thời gian.4 Sự dịch chuyển trong A và A0 : a, b ∈ Σi , c < Σi .1 Minh họa sự thực thi theo thời gian của giao diện.2 Minh họa phép song song (a) phép nối tiếp (b).3 Minh họa ôtômát khoảng giao diện và môi trường .1 Minh họa văn phạm của các định danh.2 Minh họa văn phạm của số nguyên.3 Minh họa văn phạm của các thuộc tính.4 Minh họa văn phạm của thành phần tài nguyên trong thành phần phần mềm.118 v TIEU LUAN MOI download : skknchat@gmail.5 Minh họa văn phạm của tài nguyên hệ thống.6 Minh họa văn phạm của khoảng thời gian.7 Minh họa văn phạm của các khẳng định.8 Minh họa văn phạm của các bất biến.9 Minh họa văn phạm của các bất biến tài nguyên.10 Minh họa văn phạm của các biểu thức đơn giản.11 Minh họa văn phạm của các biểu thức trong đặc tả hệ thống.12 Minh họa văn phạm của các thành phần cơ bản.13 Minh họa văn phạm cho đặc tả phương thức.14 Minh họa văn phạm của thành phần phần mềm.15 Minh họa văn phạm của phương thức trong phần mã nguồn.16 Minh họa văn phạm của thành phần phần mềm chủ động.17 Minh họa văn phạm của hệ thống. 127 vi TIEU LUAN MOI download : [e-mail] Danh mục bảng 3.1 Bảng so sánh các mô hình thành phần phần mềm hiện tại .2 Các toán tử tăng giảm các thành phần tài nguyên . 56 vii TIEU LUAN MOI download : skknchat@gmail.94801 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. Trương Anh Hoàng 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. Hà Nội, ngày 16 tháng 8 năm 2018 Tác giả Nguyễn Trịnh Đông (LUAN.94801 TIEU LUAN MOI download : skknchat@gmail.94801 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. Trương Anh Hoàng. Tôi xin bày tỏ lòng biết ơn sâu sắc tới các thầy đã quan tâm, hướng dẫn từ các kỹ năng cơ bản đến định hướng khoa học, tạo điều kiện thuận lợi trong suốt quá trình nghiên cứu tại Trường. Tôi 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 học tập và nghiên cứu tại Trường, các kết quả khoa học trong luận án đã 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. Tôi 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 để tôi có được môi trường nghiên cứu 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à các phòng ban về sự hỗ trợ và cộng tác hiệu quả trong quá trình làm việc. Tôi 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 đồng nghiệp đã tạo nhiều thuận lợi hỗ trợ cho tôi có đủ điều kiện thực hiện đề tài nghiên cứu. Tôi 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ố được 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, tôi bày tỏ lòng biết ơn tới bố mẹ, vợ, các 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 suốt quá trình hoàn thành luận án. Hà Nội, ngày 16 tháng 8 năm 2018 Nguyễn Trịnh Đông ix (LUAN.94801 TIEU LUAN MOI download : skknchat@gmail.94801 Danh mục từ viết tắt Từ viết tắt Từ gốc Giải thích nghĩa BA Büchi Automata Ôtômát Büchi BIP Behaviour Interaction Priority Tên của một công cụ Component-Based Real-time Hệ thống thời gian thực dựa CB-RTS System trên thành phần Component-based Software Kỹ nghệ phần mềm dựa trên CBSE Engineering thành phần Component-based Software Phát triển phần mềm dựa trên CBSD Development thành phần Common Object Request Bro- Kiến trúc trung gian yêu cầu CORBA ker Architecture đối tượng chung COM Component Object Model Mô hình đối tượng thành phần CTL Computation Tree Logic Logic cây tính toán Distributed Component Ob- Mô hình đối tượng thành phần DCOM ject Model phân tán DTS Distributed Transition System Hệ thống dịch chuyển phân tán An Environment for Composi- Môi trường cho phân tích và ECDAR tional Design and Analysis of thiết kế thành phần cho hệ Real Time Systems thống thời gian thực JML Java Modelling Language Ngôn ngữ mô hình hóa Java LTL Linear Temporal Logic Logic thời gian tuyến tính MITL Metric Interval Temporal Logic Logic thời khoảng tuyến tính Markov Reward Model Tên công cụ kiểm chứng mô MRMC Checker hình Các hệ thống thành phần phần PECOS Pervasive Component Systems mềm phổ biến x (LUAN.94801 TIEU LUAN MOI download : skknchat@gmail.94801 Từ viết tắt Từ gốc Giải thích nghĩa Bộ kiểm chứng mô hình xác PRISM Probabilistic Model Checker suất PTA Priced Timed Automaton Ôtômát trọng số RTS Real-time systems Hệ thống thời gian thực A refinement calculus for ob- Sự tinh giảm tính toán cho các rCOS ject systems hệ thống đối tượng Ngôn ngữ mô hình hóa hệ SysML System Modeling Language thống A Tool for Modeling and Công cụ cho sự thực thi và mô TIMES Implementation of Embedded hình hóa của hệ thống nhúng Systems Công cụ kiểm chứng thời gian Uppsala University and Aal- UPPAAL thực do hai trường đại học borg University cùng phát triển UPPAAL Uppaal - Statistical Model Công cụ kiểm chứng mô hình - SMC Checker thống kê dựa trên UPPAAL TA Timed Automata Ôtômát thời gian Timed Computational Tree TCTL Logic cây tính toán thời gian Logic Unifying Theories of Program- Lý thuyết hợp nhất ngôn ngữ UTP ming lập trình Tên của một công cụ do nhóm X-MAN X-MAN tác giả Nannan He, K. Lau phát triển WCET Worst-case Execution Time Thời gian thực thi lớn nhất (LUAN.94801 TIEU LUAN MOI download : skknchat@gmail.94801 Danh mục các ký hiệu ν Phép gán các giá trị đồng hồ (clock interpretation) 17 Σi Bảng chữ cái thứ i 37 2{ Tập powerset của tập đồng hồ trong ôtômát thời gian 17 [b, e] Khoảng thời gian 68 { Tập đồng hồ 17  Lớp tương đương 19 ∆ Độ lệch thời gian tối thiểu giữa hai hành động 16 ð Thể thức tương tác thời gian thực có ràng buộc tài nguyên 52 Γ Tập các vị trí chấp thuận (đến) được trong ôtômát thời gian 17 ~ Tập đồng hồ được thiết lập lại giá trị sau mỗi bước chuyển của ôtômát thời gian 17 λ Hàm gán nhãn 20 h`, νi Một trạng thái của ôtômát thời gian 17 bν(x)c Phần nguyên của giá trị các đồng hồ 19 brc Phần nguyên của số thực r 42 C Thành phần phần mềm 11 Ei Biểu thức chính quy thứ i 37 N Tập số tự nhiên 17 xii (LUAN.94801 TIEU LUAN MOI download : skknchat@gmail.