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.
