|
Abstract:
|
Trong thời đại ngày nay, các hệ thống có yếu tố thời gian và đặc biệt các hệ thống
thời gian thực là một trong những lĩnh vực nhận được rất nhiều sự quan tâm của giới
khoa học nói chung và giới khoa học nghiên cứu về công nghệ nói riêng. Thật vây, hệ
thống thời gian thực được ứng dụng rất nhiều trong đời sống xã hội, trong sản xuất,
trong y tế, trong hàng không vũ trụ và trong quân sự, gần như trong mọi lĩnh vực ta
đều thấy có sự góp mặt của những ứng dụng trong hệ thống thời gian thực. Không chỉ
góp mặt trong nhiều lĩnh vực mà sự góp mặt của nó còn có tầm quan trọng rất lớn đối
với hệ thống. Trong hệ thống thời gian thực, các công vệ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ệ Hard
Real- Time) hoặc sẽ bị suy giảm về chất lượng dịch vụ (hệ 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. Tuy nhiên, việc
đặc tả và kiểm chứng một hệ thống thời gian thực là một bài toán khó và một trong
những mối quan tâm lớn hiện nay là làm thế nào để đặc tả và kiểm chứng tự động cho
các hệ thống thời gian thực.
Bộ công cụ Uppaal ra đời phần nào đáp ứng được yêu cầu đó, công cụ này giúp ta có
thể kiểm định những hệ thống được mô hình hóa thành những hệ thống automata thời
gian với nhứng 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. |