TAPAAL Model tekshiruvi - TAPAAL Model Checker
| Tuzuvchi (lar) | Olborg universiteti |
|---|---|
| Dastlabki chiqarilish | 2008 |
| Barqaror chiqish | 3.6.1 / 2020 yil 18-mart |
| Yozilgan | C ++ va GUI yilda Java |
| Operatsion tizim | Linux Mac OS X Microsoft Windows |
| Mavjud: | Ingliz tili |
| Turi | Modelni tekshirish |
| Litsenziya | Ochiq manba |
| Veb-sayt | http://www.tapaal.net |
TAPAAL modellashtirish uchun vosita, simulyatsiya va tekshirish ning Vaqt o'tqazilgan Petri to'rlari Kompyuter fanlari kafedrasida ishlab chiqilgan Olborg universiteti Daniyada va Linux, Windows va Mac OS X platformalarida mavjud.[1]
Timed-Arc Petri Net (TAPN) klassikaning vaqtni kengaytirishi Petri to'ri model (tomonidan tarqatilgan hisoblashlarning keng tarqalgan ishlatiladigan grafik modeli Karl Adam Petri 1962 yildagi dissertatsiyasida). TAPN-da ko'rib chiqilgan vaqtni uzaytirish real vaqt rejimiga aniq munosabatda bo'lishga imkon beradi, bu tarmoqdagi belgilar bilan bog'liq (har bir belgi o'z yoshiga ega) va joylardan o'tish joylariga yoylar vaqt belgilarini yoshini cheklaydigan vaqt oralig'ida belgilanadi. tegishli o'tishni yoqish uchun ishlatilishi mumkin. TAPAAL vositasida ushbu modelni transport yoylari (masalan, ilgari o'qish-o'qi deb qaralgandan ko'ra ko'proq ifodalaydi) va inhibitor kamonlari bilan yoshi o'zgaruvchanligi bilan yanada kengaytirish amalga oshiriladi.
TAPAAL vositasi TAPN modellarini chizish uchun grafik muharriri, mo'ljallangan to'rlar bilan tajriba o'tkazish uchun simulyator va tasdiqlash muhitini taklif qiladi, bu avtomatik ravishda mantiqiy so'rovlarga javob beradi. CTL mantiq (asosan EF, EG, AF, AG formulalari joylashtirmasdan). Shuningdek, u foydalanuvchiga ma'lum bir k uchun k berilgan chegarasi berilganligini tekshirishga imkon beradi. TAPAAL TAPAAL bilan birgalikda tarqatiladigan o'zlarining tasdiqlash dvigatellari bilan jihozlangan (doimiy ravishda bitta)[2] va alohida vaqt uchun[3] ). Ixtiyoriy ravishda foydalanuvchi TAPAAL modellarini avtomatik ravishda tarjima qilishi mumkin UPPAAL va ga ishoning UPPAAL tekshirish mexanizmi.
Tashqi havolalar
- TAPAAL veb-sayti, yuklab olish
- DES bo'limi, Daniya, Olborg universiteti, Kompyuter fanlari fakulteti
- TAPAAL: J. Byg, K.Y.ning muharriri, Timed-Arc Petri Nets-ning simulyatori va tekshiruvchisi. Yorgensen va J. Srba, ATVA'09, Springer
- Timed-Arc Petri Nets-ni vaqtli avtomatika tarmoqlariga samarali tarjimasi J. Byg, K.Y. Yorgensen va J. Srba, ICFEM'09, Springer
- Vaqt o'tishi bilan bog'liq tizimlar va TCTL modelini saqlab qolish uchun asos. Jeykobsen, M. Jakobsen, M.X. Moller va J. Srba, EPEW'10, Springer
- Timed-Arc Petri Nets-ning tekshiruvi L. Yakobsen, M. Yakobsen, M.X. Moller va J. Srba, SOFSEM'11, Springer
Adabiyotlar
- ^ Aleksandr Devid; Lasse Jacobsen; Morten Jacobobsen; Kennet Yrke Yorgensen; Mikael H. Moller; Jiří Srba (2012). "TAPAAL 2.0: Tayyorlangan ark Petri Nets uchun kompleks rivojlanish muhiti". TACAS. LNCS. 7214: 492–497. doi:10.1007/978-3-642-28756-5_36. ISBN 978-3-642-28755-8.
- ^ Aleksandr Devid; Lasse Jacobsen; Morten Jacobobsen; Jiří Srba (2012). "Chegaralangan vaqt oralig'idagi Petri to'rlari uchun oldinga etib borish algoritmi". SSV. EPTCS. 102: 141–155. arXiv:1211.6194. doi:10.4204 / EPTCS.102.12.
- ^ M. Andersen LarsenJ. SrbaM.G. Sørensen J.H. Taankvist (2012). "Petri to'rlari yopiq vaqt ichida jonli xususiyatlarini tekshirish". MEMIKA. LNCS: 69-81.
 | Bu rasmiy usullar bilan bog'liq maqola a naycha. Siz Vikipediyaga yordam berishingiz mumkin uni kengaytirish. |