Uppaal Model Checker


UPPAAL — это интегрированная инструментальная среда для моделирования , валидации и верификации систем реального времени , смоделированных как сети синхронизированных автоматов , дополненных типами данных (ограниченные целые числа, массивы и т. д.).

Он использовался как минимум в 17 тематических исследованиях с момента его выпуска в 1995 году, в том числе в Lego Mindstorms , для аудиопротокола Philips и в контроллерах коробки передач для Mecel . [1]

Инструмент был разработан в сотрудничестве между группой проектирования и анализа систем реального времени Упсальского университета , Швеция , и фундаментальными исследованиями в области компьютерных наук Ольборгского университета , Дания .