Программа проверки моделей TAPAAL - TAPAAL Model Checker
| Разработчики) | Ольборгский университет |
|---|---|
| изначальный выпуск | 2008 |
| Стабильный выпуск | 3.6.1 / 18 марта 2020 г. |
| Написано в | C ++ и GUI в Ява |
| Операционная система | Linux Mac OS X Майкрософт Виндоус |
| Доступно в | английский |
| Тип | Проверка модели |
| Лицензия | Открытый исходный код |
| Интернет сайт | http://www.tapaal.net |
ТАПААЛ инструмент для моделирования, симуляция и проверка из Сети Петри с временной дугой разработан на кафедре компьютерных наук Ольборгский университет в Дании и доступен для платформ Linux, Windows и Mac OS X.[1]
Timed-Arc Petri Net (TAPN) - это временное расширение классической Сеть Петри модель (обычно используемая графическая модель распределенных вычислений, представленная Карл Адам Петри в его диссертации в 1962 г.). Расширение времени, рассматриваемое в TAPN, позволяет явно обрабатывать данные в реальном времени, которые связаны с токенами в сети (каждый токен имеет свой возраст), а дуги от мест к переходам помечены временными интервалами, которые ограничивают возраст токенов, которые может использоваться для запуска соответствующего перехода. В инструменте TAPAAL реализовано дальнейшее расширение этой модели с инвариантами возраста с транспортными дугами (которые более выразительны, чем, например, ранее рассмотренные дуги чтения) и с дугами-ингибиторами.
Инструмент TAPAAL предлагает графический редактор для рисования моделей TAPN, симулятор для экспериментов с разработанными сетями и среду проверки, которая автоматически отвечает на логические запросы, сформулированные в подмножестве CTL логика (в основном формулы EF, EG, AF, AG без вложенности). Это также позволяет пользователю проверить, является ли данная сеть k-ограниченной для данного числа k. TAPAAL оснащен собственными механизмами проверки, распространяемыми вместе с TAPAAL (один для непрерывного времени[2] и один для дискретного времени[3] ). При желании пользователь может автоматически переводить модели TAPAAL в UPPAAL и полагаться на UPPAAL двигатель проверки.
внешняя ссылка
- Сайт ТАПААЛ, скачать
- Подразделение DES, Департамент компьютерных наук, Университет Ольборга, Дания
- TAPAAL: редактор, симулятор и верификатор сетей Петри с временной дугой, автор J. Byg, K.Y. Йоргенсен и Дж. Срба, ATVA'09, Springer
- Эффективный перевод сетей Петри с временной дугой в сети временных автоматов, автор J. Byg, K.Y. Йоргенсен и Дж. Срба, ICFEM'09, Springer
- Структура связи систем с синхронизированным переходом и сохранения проверки модели TCTL. Авторы: L. Jacobsen, M. Jacobsen, M.H. Мёллер и Дж. Срба, EPEW'10, Springer
- Верификация сетей Петри с временной дугой, выполненная Л. Якобсеном, М. Якобсеном, М. Мёллер и Дж. Срба, SOFSEM'11, Springer
Рекомендации
- ^ Александр Давид; Лассе Якобсен; Мортен Якобсен; Кеннет Юрке Йоргенсен; Микаэль Х. Мёллер; Иржи Срба (2012). "TAPAAL 2.0: Интегрированная среда разработки для сетей Петри с временной дугой". ТАКАС. LNCS. 7214: 492–497. Дои:10.1007/978-3-642-28756-5_36. ISBN 978-3-642-28755-8.
- ^ Александр Давид; Лассе Якобсен; Мортен Якобсен; Иржи Срба (2012). "Алгоритм прямой достижимости для ограниченных сетей Петри с временной дугой". SSV. EPTCS. 102: 141–155. arXiv:1211.6194. Дои:10.4204 / EPTCS.102.12.
- ^ М. Андерсен ЛарсенДж. SrbaM.G. SørensenJ.H. Таанквист (2012). "Проверка живучести закрытых сетей Петри с временной дугой". МЕМИКА. LNCS: 69–81.
 | Этот формальные методы -связанная статья является заглушка. Вы можете помочь Википедии расширяя это. |