WikiDer > PAT (проверка моделей)

PAT (model checker)
PAT
Разработчики)Национальный университет Сингапура
изначальный выпуск2008 (2008)
Стабильный выпуск
3.5.1 / 13 августа 2013 г.; 7 лет назад (2013-08-13)
Написано вC #
Операционная системаМайкрософт Виндоус; Linux, Unix, Mac OS X с Мононуклеоз
Платформа.Net 3.0
Доступно ванглийский
Упрощенный китайский)
Китайский традиционный)
Японский
Немецкий
вьетнамский
ТипПроверка модели
Интернет сайтhttp://pat.comp.nus.edu.sg/

PAT (Process Analysis Toolkit) - это автономная среда[1] для создания, моделирования и анализа параллельных систем реального времени и других возможных областей. Он поставляется с удобным интерфейсом, редактором моделей и анимированным симулятором. Самое главное, что PAT реализует различные проверка модели методы, обслуживающие различные свойства, такие как тупик-свободность, расхождение-свободность, доступность, LTL свойства с предположения о справедливости, проверка уточнения и проверка вероятностной модели. Для достижения хорошей производительности в PAT реализованы передовые методы оптимизации, например редукция частичного порядка, снижение симметрии, абстракция счетчика процессов.[2] На данный момент PAT имеет 1350 зарегистрированных пользователей из 302 организаций из 41 страны и региона.

Рекомендации

  1. ^ Ян Лю, Джун Сун и Цзинь Сон Донг. (2011),Расширяемая архитектура для создания средства проверки многодоменных моделей. ISSRE 2011
  2. ^ Дж. Сан, Ю. Лю, А. Ройчоудхури, С. Лю и Дж. С. Донг. (2009), Справедливая проверка модели с абстракцией счетчика процессов. FM '09 Труды 2-го Всемирного конгресса по формальным методам. Дои:10.1007/978-3-642-05089-3_9

внешняя ссылка