Программа проверки моделей TAPAAL
| Разработчик(и) | Ольборгский университет |
|---|---|
| Первоначальный выпуск | 2008 |
| Стабильная версия | 3.9.4 / 24 января 2023 г |
| Написано в | C++ и графический интерфейс в Java |
| Операционная система | Линукс Мак ОС Х Microsoft Windows |
| Доступно в | Английский |
| Тип | Проверка модели |
| Лицензия | Открытый исходный код |
| Веб-сайт | http://www.tapaal.net |
TAPAAL — это инструмент для моделирования, имитации и проверки сетей Петри с временной дугой, разработанный на факультете компьютерных наук Ольборгского университета в Дании и доступный для платформ Linux, Windows и Mac OS X. [1]
Сеть Петри с временной дугой (TAPN) представляет собой временное расширение классической модели сети Петри (широко используемой графической модели распределенных вычислений, представленной Карлом Адамом Петри в его диссертации в 1962 году). Расширение времени, рассматриваемое в TAPN, допускает явную обработку реального времени, которое связано с токенами в сети (каждый токен имеет свой возраст), а дуги от мест до переходов помечаются временными интервалами, которые ограничивают возраст токенов, которые может использоваться для запуска соответствующего перехода. В инструменте TAPAAL реализовано дальнейшее расширение этой модели возрастными инвариантами с транспортными дугами (которые более выразительны, чем, например, ранее рассмотренные дуги чтения) и с ингибиторными дугами.
Инструмент TAPAAL предлагает графический редактор для рисования моделей TAPN, симулятор для экспериментов с спроектированными сетями и среду проверки, которая автоматически отвечает на логические запросы, сформулированные в подмножестве логики CTL (по сути, формулы EF, EG, AF, AG без вложенности). Это также позволяет пользователю проверить, является ли данная сеть k-ограниченной для данного числа k. TAPAAL оснащен собственными механизмами проверки, распространяемыми вместе с TAPAAL (один для непрерывного [2] и один для дискретного времени [3] ). При желании пользователь может автоматически переводить модели TAPAAL. в UPPAAL и положитесь на механизм проверки UPPAAL .
Внешние ссылки
[ редактировать ]- сайт ТАПААЛ, скачать
- Подразделение DES, факультет компьютерных наук, Ольборгский университет, Дания
- TAPAAL: Редактор, симулятор и верификатор сетей Петри с временной дугой, авторы Дж. Бюг, К. К. Йоргенсен и Дж. Срба, ATVA'09, Springer
- «Эффективный перевод сетей Петри с временными дугами в сети временных автоматов», Дж. Бюг, К. К. Йоргенсен и Дж. Срба, ICFEM'09, Springer
- Структура связи систем временных переходов и сохранение проверки модели TCTL Л. Якобсен, М. Якобсен, М. Мёллер и Дж. Срба, EPEW'10, Springer
- Верификация сетей Петри с временной дугой, проведенная Л. Якобсеном, М. Якобсеном, М. Мёллером и Дж. Србой, SOFSEM'11, Springer
Ссылки
[ редактировать ]- ^ Александр Давид; Лассе Якобсен; Мортен Якобсен; Кеннет Ирк Йоргенсен; Микаэль Х. Моллер; Иржи Срба (2012). «TAPAAL 2.0: Интегрированная среда разработки для сетей Петри с временной дугой». Инструменты и алгоритмы построения и анализа систем . ЛНКС. Том. 7214. стр. 492–497. дои : 10.1007/978-3-642-28756-5_36 . ISBN 978-3-642-28755-8 .
- ^ Александр Давид; Лассе Якобсен; Мортен Якобсен; Иржи Срба (2012). «Алгоритм прямой достижимости для ограниченных сетей Петри с временной дугой». Электронные труды по теоретической информатике . 102 : 141–155. arXiv : 1211.6194 . дои : 10.4204/EPTCS.102.12 . S2CID 15499812 .
- ^ М. Андерсен Х.Г. Ларсен Дж. СрбаМ.Г. СоренсенДж.Х. Таанквист (2012). «Проверка свойств живучести замкнутых сетей Петри с временной дугой». Математические и инженерные методы в информатике . ЛНКС. Том. 7721. стр. 69–81. дои : 10.1007/978-3-642-36046-6_8 . ISBN 978-3-642-36044-2 .
 | Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее . |