UPPAAL

UPPAAL это интегрированная среда инструмент для моделирования, проверки и верификации систем реального времени смоделированных как сети приурочен автоматов, расширенных с типами данных (ограниченных целых чисел, массивов и т.д.).
UPPAAL КОРА является филиалом UPPAAL для оптимального Стоимость достижимости Anslysis разработан UPPAAL команды в рамках VHS и Аметист проектов. В то время как UPPAAL поддерживает проверку модели приурочен автоматов, UPPAAL КОРА использует расширение приурочен автоматов под названием LPTA. LPTA позволяет аннотировать модель с понятием стоимости.
Это может быть стоимость задержки в определенных ситуациях или стоимости конкретных действий. Затем UPPAAL КОРА находит оптимальные пути, соответствующие условия голов.
UPPAAL КОРА был использован в ряде тематических исследований. Некоторые из них описаны на странице социологического исследования данного сайта. Если вы приехали с интересными использования, пожалуйста, свяжитесь с нами. Мы заинтересованы услышать, что вы делаете!
Из-за различных внутренних структур данных, UPPAAL КОРА настоящее время состоит из двух различных вариантах:
Версия для упрощенного случая оптимальное время анализа достижимости.
Версия для полного языке LPTA.
Как UPPAAL, UPPAAL Кора бесплатно некоммерческого использования, например, для оценки, исследования и учебных целей.
Вот некоторые ключевые особенности "UPPAAL":
Прочная
 
· Язык моделирование UPPAAL КОРА является надежной к изменениям в задаче образцу. Это означает, что инвестиции в моделировании не теряется, когда изменяется проблема, так как легко адаптировать существующие модели.
 
Быстро
 
· Хотя технология является относительно новым, экспериментальным и очень отличается от методов, используемых в традиционных оперативных исследований, UPPAAL КОРА является конкурентоспособной в ряде тематических исследований.
 
Совместимый
 
· Язык UPPAAL КОРА является расширением UPPAAL. Любой действительный UPPAAL модель также является действительным модель UPPAAL Кора. Это делает его легким и удобным для повторного использования и адаптации существующих моделей UPPAAL Кора.
 
Текущий
 
· UPPAAL КОРА основан на последней версии внутреннего развития UPPAAL, содержащий последние улучшения производительности и языка. Это, однако, экспериментальный инструмент и не хватает многих функций проверочных UPPAAL.
Ограничения:
UPPAAL КОРА с полной поддержкой LPTA имеет ряд ограничений. Эти ограничения не являются принципиальными, но являются результатом использования новых внутренних структур данных с ограниченной настоящее время набор функций. Со временем, эти ограничения будут решены.
- Нет экстраполяция, следовательно, прекращение не не гарантируется, если вы не гарантирует, что либо:
· Система ациклические.
· Все часы ограничены инвариантов.
- Простой достижимость только:
Не · Нет проверка живучести
Не · Нет проверка тупик
- Ограниченное использование направляющей:
· Поддержка (стоимость + оставшееся) сортировка осуществляется (лучший первый поиск)
· Поддержка эвристического переменной будет реализован, но выражение не может ссылаться на переменные затраты.
Что нового в этой версии:
Этот выпуск исправляет ошибки краш и утечка памяти.