Đặc tả và kiểm chứng các hệ thống thời gian thực sử dụng Uppaal

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.