Narzędzie do sprawdzania modeli TAPAAL
| Deweloperzy | Uniwersytet w Aalborgu |
|---|---|
| Pierwsze wydanie | 2008 |
| Wersja stabilna | 3.9.4 / 24 stycznia 2023 r.
|
| Napisane w | C++ i GUI w Javie |
| System operacyjny |
Linux Mac OS X Microsoft Windows |
| Dostępne w | język angielski |
| Typ | Sprawdzenie modelu |
| Licencja | Otwarte źródło |
| Strona internetowa | http://www.tapaal.net |
TAPAAL to narzędzie do modelowania, symulacji i weryfikacji sieci Petriego z łukiem czasowym opracowane na Wydziale Informatyki Uniwersytetu Aalborg w Danii i dostępne na platformy Linux, Windows i Mac OS X.
Timed-Arc Petri Net (TAPN) to rozszerzenie czasowe klasycznego modelu sieci Petriego (powszechnie używany graficzny model obliczeń rozproszonych wprowadzony przez Carla Adama Petriego w rozprawie z 1962 r.). Rozszerzenie czasu rozważane w TAPN pozwala na jednoznaczne traktowanie czasu rzeczywistego, który jest powiązany z tokenami w sieci (każdy token ma swój wiek), a łuki od miejsc do przejść są oznaczane interwałami czasowymi, które ograniczają wiek tokenów, które może być użyty do odpalenia odpowiedniego przejścia. W narzędziu TAPAAL zaimplementowano dalsze rozszerzenie tego modelu o niezmienniki wieku z łukami transportowymi (które są bardziej wyraziste niż na przykład rozważane wcześniej łuki odczytu) oraz z łukami hamującymi.
Narzędzie TAPAAL oferuje edytor graficzny do rysowania modeli TAPN, symulator do eksperymentowania z zaprojektowanymi sieciami oraz środowisko weryfikacyjne, które automatycznie odpowiada na zapytania logiczne sformułowane w podzbiorze logiki CTL (zasadniczo formuły EF, EG, AF, AG bez zagnieżdżania). Pozwala również użytkownikowi sprawdzić, czy dana sieć jest k-ograniczona dla danej liczby k. TAPAAL jest wyposażony we własne silniki weryfikacyjne dystrybuowane razem z TAPAAL (jeden dla czasu ciągłego i jeden dla czasu dyskretnego). Opcjonalnie użytkownik może automatycznie tłumaczyć modele TAPAAL na UPPAAL i polegać na UPPAAL silnik weryfikacji.
Linki zewnętrzne
- Strona TAPAAL, pobierz
- Jednostka DES, Wydział Informatyki Uniwersytetu Aalborg, Dania
- TAPAAL: edytor, symulator i weryfikator sieci Petriego z łukiem czasowym autorstwa J. Byga, KY Jørgensena i J. Srby, ATVA'09, Springer
- Wydajne tłumaczenie sieci Petriego z łukiem czasowym na sieci automatów czasowych J. Byg, KY Jørgensen i J. Srba, ICFEM'09, Springer
- A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking autorstwa L. Jacobsena, M. Jacobsena, MH Møllera i J. Srby, EPEW'10, Springer
- Weryfikacja siatek Petriego z łukiem czasowym przeprowadzona przez L. Jacobsena, M. Jacobsena, MH Møllera i J. Srbę, SOFSEM'11, Springer
- Bibliografia _ Lasse Jacobsena; Mortena Jacobsena; Kenneth Yrke Jørgensen; Mikaela H. Møllera; Jiří Srba (2012). „TAPAAL 2.0: zintegrowane środowisko programistyczne dla sieci Petriego z łukiem czasowym” . Narzędzia i algorytmy do budowy i analizy systemów . LNCS. Tom. 7214. s. 492–497. doi : 10.1007/978-3-642-28756-5_36 . ISBN 978-3-642-28755-8 .
- Bibliografia _ Lasse Jacobsena; Mortena Jacobsena; Jiří Srba (2012). „Algorytm osiągalności do przodu dla sieci Petriego z ograniczonym łukiem czasowym”. Postępowanie elektroniczne w informatyce teoretycznej . 102 : 141–155. ar Xiv : 1211.6194 . doi : 10.4204/EPTCS.102.12 . S2CID 15499812 .
- Bibliografia _ LarsenJ. Srba M.G. SørensenJ.H. Taankvist (2012). „Weryfikacja właściwości żywości w sieciach Petriego z zamkniętym łukiem czasowym”. Metody matematyczne i inżynierskie w informatyce . LNCS. Tom. 7721. s. 69–81. doi : 10.1007/978-3-642-36046-6_8 . ISBN 978-3-642-36044-2 .