I. Tổng Quan Nghiên Cứu Hệ Thống Thời Gian Thực Với UPPAAL
Trong kỷ nguyên số, hệ thống thời gian thực ngày càng đóng vai trò quan trọng trong nhiều lĩnh vực, từ công nghiệp, y tế đến hàng không vũ trụ và quân sự. Đặc biệt, các hệ thống này đòi hỏi sự chính xác và tin cậy cao về thời gian. Nếu không đáp ứng được yêu cầu thời gian, hệ thống có thể sụp đổ hoặc gây ra hậu quả nghiêm trọng. Do đó, việc kiểm tra tính đúng đắn của hệ thống là vô cùng cần thiết. UPPAAL là một công cụ mạnh mẽ để mô hình hóa, mô phỏng và kiểm chứng các hệ thống thời gian thực. Công cụ này cho phép kiểm chứng các hệ thống được mô hình hóa thành các hệ thống automata thời gian với các biến số nguyên, cấu trúc dữ liệu, hàm người dùng và đồng bộ các kênh. Việc sử dụng UPPAAL trong kiểm chứng hệ thống có yếu tố thời gian đòi hỏi người sử dụng có trình độ nhất định trong việc đặc tả hệ thống dưới dạng các automata thời gian cũng như điều khiển sự vận hành và tương tác giữa các automata đó thông qua một ngôn ngữ lập trình.
1.1. Tầm Quan Trọng của Hệ Thống Thời Gian Thực
Hệ thống thời gian thực được ứng dụng rộng rãi trong đời sống xã hội, sản xuất, y tế, hàng không vũ trụ và quân sự. Trong hệ thống thời gian thực, các công việc và các tác vụ cần phải hoàn thành trong một khoảng thời gian cho phép (deadline). Nếu không đáp ứng được yêu cầu thời gian thì hệ thống sẽ sụp đổ hoặc sẽ gây ra hậu quả nghiêm trọng (hệ thời gian thực cứng: hard Real-Time) hoặc sẽ bị suy giảm về chất lượng dịch vụ (hệ thời gian thực mềm: Soft Real-Time). Chính vì tầm quan trọng của yếu tố thời gian trong hệ thống thời gian thực như vậy nên việc kiểm tra tính đúng đắn đối với hệ thống này là rất cần thiết.
1.2. Giới Thiệu Công Cụ UPPAAL cho Mô Hình Hóa
UPPAAL là một công cụ mạnh mẽ để mô hình hóa, mô phỏng và kiểm chứng các hệ thống thời gian thực. Công cụ này cho phép kiểm chứng các hệ thống được mô hình hóa thành các hệ thống automata thời gian với các biến số nguyên, cấu trúc dữ liệu, hàm người dùng và đồng bộ các kênh. Với việc đặc tả và kiểm chứng một hệ thống thời gian thực thì bộ công cụ UPPAAL được đánh giá là tốt nhất hiện nay và được sử dụng rộng rãi trong công nghiệp.
II. Thách Thức và Giải Pháp Kiểm Chứng với UPPAAL
Việc kiểm tra tính đúng đắn của một hệ thống có thể được thực hiện ở khâu kiểm thử và kiểm chứng. Tuy nhiên, với những hệ thống có ràng buộc về thời gian cũng như tầm quan trọng của hệ thống mà việc kiểm thử không kiểm tra được hết mà chủ yếu tập trung ở khâu kiểm chứng. Việc kiểm chứng tính đúng đắn của hệ thống nhằm kiểm tra xem hệ thống có vận hành đúng như yêu cầu không, muốn vậy cần phải có mô phỏng sự vận hành của hệ thống, cần có bước kiểm tra quy trình vận hành đó có đảm bảo các tính chất cơ bản của một hệ thống như: tính đến được của một trạng thái, tính an toàn, tính liên tục theo thời gian (không bị dừng – not deadlock). Muốn làm được điều đó cần phải có một bộ công cụ có thể mô tả được sự vận hành của hệ thống, qua đó mô phỏng được sự vận hành đó và từ đó kiểm tra được sự vận hành đó có thỏa mãn các yêu cầu của hệ thống hay không.
2.1. Vấn Đề Kiểm Chứng Tính Đúng Đắn Hệ Thống
Việc kiểm tra tính đúng đắn của một hệ thống có thể được thực hiện ở khâu kiểm thử và kiểm chứng. Tuy nhiên, với những hệ thống có ràng buộc về thời gian cũng như tầm quan trọng của hệ thống mà việc kiểm thử không kiểm tra được hết mà chủ yếu tập trung ở khâu kiểm chứng. Việc kiểm chứng tính đúng đắn của hệ thống nhằm kiểm tra xem hệ thống có vận hành đúng như yêu cầu không, muốn vậy cần phải có mô phỏng sự vận hành của hệ thống.
2.2. Giải Pháp Mô Phỏng và Kiểm Tra Vận Hành
Cần phải có một bộ công cụ có thể mô tả được sự vận hành của hệ thống, qua đó mô phỏng được sự vận hành đó và từ đó kiểm tra được sự vận hành đó có thỏa mãn các yêu cầu của hệ thống hay không. Đây thực sự là mối quan tâm lớn đối với vấn đề kiểm chứng nói riêng và công nghệ phần mềm nói chung.
III. Phương Pháp Đặc Tả và Kiểm Chứng Hệ Thống với UPPAAL
Trong luận văn này tác giả đã tập trung tìm hiểu về bộ công cụ kiểm chứng UPPAAL, đi sâu vào tìm hiểu ngôn ngữ đặc tả của UPPAAL, tìm hiểu cách đặc tả một hệ thống phần mềm dưới dạng các automata thời gian và điều khiển sự vận hành của hệ thống thông qua ngôn ngữ lập trình C++, cũng như tìm hiểu cơ chế kiểm chứng của bộ công cụ này cho các hệ thống thời gian thực. Từ đó tác giả xây dựng một số ví dụ (cụ thể tác giả đã xây dựng được 4 ví dụ) về một số hệ thống thời gian thực áp dụng vào đặc tả và kiểm chứng hệ thống đó bởi bộ công cụ UPPAAL. Đối với mỗi ví dụ tác giả giả định là một hệ thống thời gian thực, tiến hành đặc tả, mô hình hóa dưới hệ ô-tô-mát thời gian trên trình soạn thảo của UPPAAL sau đó chạy mô phỏng và kiểm chứng sự hoạt động của hệ thống đó.
3.1. Tìm Hiểu Ngôn Ngữ Đặc Tả của UPPAAL
Tác giả đã tập trung tìm hiểu về bộ công cụ kiểm chứng UPPAAL, đi sâu vào tìm hiểu ngôn ngữ đặc tả của UPPAAL, tìm hiểu cách đặc tả một hệ thống phần mềm dưới dạng các automata thời gian và điều khiển sự vận hành của hệ thống thông qua ngôn ngữ lập trình C++, cũng như tìm hiểu cơ chế kiểm chứng của bộ công cụ này cho các hệ thống thời gian thực.
3.2. Xây Dựng Ví Dụ Thực Tế và Kiểm Chứng
Từ đó tác giả xây dựng một số ví dụ (cụ thể tác giả đã xây dựng được 4 ví dụ) về một số hệ thống thời gian thực áp dụng vào đặc tả và kiểm chứng hệ thống đó bởi bộ công cụ UPPAAL. Đối với mỗi ví dụ tác giả giả định là một hệ thống thời gian thực, tiến hành đặc tả, mô hình hóa dưới hệ ô-tô-mát thời gian trên trình soạn thảo của UPPAAL sau đó chạy mô phỏng và kiểm chứng sự hoạt động của hệ thống đó.
IV. Ứng Dụng UPPAAL Mô Hình Hóa Hệ Thống Điều Khiển
Trong chương 4, tác giả trình bày một số ví dụ áp dụng mà tác giả đã xây dựng được sau khi tìm hiểu về bộ công cụ UPPAAL. Chương này tác giả trình bày bốn ví dụ mà tác giả đã xây dựng được về bốn hệ thống thời gian và tiến hành đặc tả và kiểm chứng các hệ thống đó qua công cụ UPPAAL. Các ví dụ bao gồm hệ thống điều khiển sử dụng vùng tài nguyên, hệ thống điều khiển việc sử dụng chung vùng tài nguyên Process Resource V1 (có ràng buộc về thời gian sử dụng nguồn tài nguyên) và hệ thống điều khiển việc sử dụng chung vùng tài nguyên Process Resource V2 (có nhiều nhóm quá trình có ràng buộc về thời gian sử dụng nguồn tài nguyên).
4.1. Hệ Thống Điều Khiển Sử Dụng Vùng Tài Nguyên
Ví dụ về hệ thống điều khiển sử dụng vùng tài nguyên được mô hình hóa và kiểm chứng bằng UPPAAL. Mục tiêu là đảm bảo việc sử dụng tài nguyên được thực hiện đúng thời gian và không gây ra xung đột.
4.2. Hệ Thống Điều Khiển Chung Vùng Tài Nguyên Process Resource V1
Hệ thống điều khiển việc sử dụng chung vùng tài nguyên Process Resource V1 (có ràng buộc về thời gian sử dụng nguồn tài nguyên) được phân tích và kiểm chứng để đảm bảo tính an toàn và hiệu quả.
4.3. Hệ Thống Điều Khiển Chung Vùng Tài Nguyên Process Resource V2
Hệ thống điều khiển việc sử dụng chung vùng tài nguyên Process Resource V2 (có nhiều nhóm quá trình có ràng buộc về thời gian sử dụng nguồn tài nguyên) được mô hình hóa và kiểm chứng để đảm bảo tính đúng đắn và hiệu suất.
V. Kết Luận và Hướng Phát Triển Nghiên Cứu UPPAAL
Luận văn đã trình bày các cơ sở lý thuyết cần thiết cho việc nghiên cứu đề tài, cũng như những hiểu biết của tác giả về bộ công cụ UPPAAL cũng như cách đặc tả một hệ thống phần mềm dưới dạng các automata thời gian và phương pháp mô phỏng và kiểm chứng trong UPPAAL. Tác giả đã xây dựng được một số ví dụ áp dụng sau khi tìm hiểu về bộ công cụ UPPAAL. Tuy nhiên, luận văn vẫn còn những hạn chế và hướng mở rộng tiếp theo của đề tài. Cần có thêm nhiều nghiên cứu sâu hơn về các tính năng nâng cao của UPPAAL và ứng dụng vào các hệ thống phức tạp hơn.
5.1. Tóm Tắt Công Việc Đã Thực Hiện
Luận văn đã trình bày các cơ sở lý thuyết cần thiết cho việc nghiên cứu đề tài, cũng như những hiểu biết của tác giả về bộ công cụ UPPAAL cũng như cách đặc tả một hệ thống phần mềm dưới dạng các automata thời gian và phương pháp mô phỏng và kiểm chứng trong UPPAAL.
5.2. Hạn Chế và Hướng Mở Rộng Nghiên Cứu
Luận văn vẫn còn những hạn chế và hướng mở rộng tiếp theo của đề tài. Cần có thêm nhiều nghiên cứu sâu hơn về các tính năng nâng cao của UPPAAL và ứng dụng vào các hệ thống phức tạp hơn.
