Проверка модели Uppaal
Разработчик(и) | Уппсальский университет Ольборгский университет |
---|---|
Первоначальный выпуск | 1995 |
Стабильная версия | 5.0.0 / 14 июля 2023 г |
Предварительный выпуск | 5.1.0-бета3 / 23 октября 2023 г |
Написано в | C++ и графический интерфейс в Java |
Операционная система | Линукс Мак ОС Х Microsoft Windows |
Доступно в | английский датский японский китайский литовский |
Тип | Проверка модели |
Лицензия | Коммерческие лицензии Академические лицензии |
Веб-сайт | http://www.uppaal.org/ http://www.uppaal.com/ |
UPPAAL — это интегрированная инструментальная среда для моделирования , проверки и верификации систем реального времени , смоделированных как сети синхронизированных автоматов , расширенных типами данных (ограниченные целые числа, массивы и т. д.).
С момента его выпуска в 1995 году он использовался как минимум в 17 тематических исследованиях, в том числе в Lego Mindstorms , для аудиопротокола Philips и в контроллерах коробки передач для Mecel . [1]
Инструмент был разработан в сотрудничестве между группой проектирования и анализа систем реального времени в Уппсальском университете , Швеция , и фундаментальными исследованиями в области компьютерных наук в Ольборгском университете , Дания .
Доступны следующие расширения:
- Cora для анализа достижимости оптимальной стоимости.
- Tron для онлайн-тестирования систем реального времени (тестирование на соответствие «черного ящика»).
- Обложка для создания оптимальных автономных тестов COVERerage.
- Tiga для синтеза контроллера на основе TImed GAmes.
- Порт для систем синхронизации на основе компонентов, использующих методы частичного уменьшения порядка.
- Pro для PRO-бабилистического анализа достижимости. (Снято с производства)
- SMC для проверки статистической модели.
Ссылки [ править ]
Внешние ссылки [ править ]
- Академический сайт УППАЛ
- Коммерческий сайт УПААЛ
- Группа «Проектирование и анализ систем реального времени»
- Подразделение DEIS, кафедра компьютерных наук ААУ