PAT (проверка модели)
| Разработчик(и) | Национальный университет Сингапура |
|---|---|
| Первоначальный выпуск | 2008 |
| Стабильная версия | 3.5.1 / 13 августа 2013 г |
| Написано в | С# |
| Операционная система | Microsoft Windows ; Linux , Unix , Mac OS X с Mono |
| Платформа | .Net 3.0 |
| Доступно в | Английский Китайский (упрощенный) Китайский (традиционный) японский немецкий вьетнамский |
| Тип | Проверка модели |
| Веб-сайт | http://pat.comp.nus.edu.sg/ |
PAT (Process Analysis Toolkit) — это автономная среда. [1] для составления, моделирования и обоснования параллельных систем реального времени и других возможных областей. Он включает в себя пользовательские интерфейсы, редактор моделей и анимированный симулятор. PAT реализует различные методы проверки модели, учитывающие различные свойства, такие как отсутствие тупиковых ситуаций и расхождений , достижимость, свойства LTL с предположениями о справедливости , уточненная проверка и вероятностная проверка модели. Для достижения хорошей производительности в PAT реализованы передовые методы оптимизации, например, частичное уменьшение порядка , уменьшение симметрии , абстракция счетчика процессов. [2]
Ссылки [ править ]
- ^ Ян Лю, Цзюнь Сун и Джин Сон Дон. (2011), Расширяемая архитектура для создания средства проверки многодоменных моделей . ИССРЭ 2011
- ^ Дж. Сан, Ю. Лю, А. Ройчудри, С. Лю и Дж. С. Донг (2009), Честная проверка модели с помощью абстракции счетчика процессов . FM '09 Материалы 2-го Всемирного конгресса по формальным методам . дои : 10.1007/978-3-642-05089-3_9