Устройство для проверки моделей Uppaal
-
Обзор инструмента UPPAAL
- UPPAAL — это среда для моделирования и верификации систем реального времени.
- Используется в 17 исследованиях, включая Lego Mindstorms и аудиопротоколы Philips.
- Разработан в сотрудничестве между университетами Уппсалы и Ольборга.
-
Расширения UPPAAL
- Cora для анализа доступности.
- Tron для онлайн-тестирования соответствия «черному ящику».
- Покрытие для автономной генерации тестов.
- Tiga для синтеза контроллеров на основе временных игр.
- Порт для синхронизации на основе методов частичного сокращения заказов.
- Профессионал в области вероятностного анализа достижимости (больше не производится).
- SMC для проверки статистической модели.
-
Рекомендации и ресурсы
- Ссылки на внешние ресурсы, включая академические и коммерческие сайты.
- Упоминание о возможности расширения статьи для Википедии.