Uppaal Model Checker - Uppaal Model Checker

UPPAAL
Tuzuvchi (lar)Uppsala universiteti
Olborg universiteti
Dastlabki chiqarilish1995 (1995)
Barqaror chiqish
4.0.14 / 20 may, 2014 yil; 6 yil oldin (2014-05-20)
Ko'rib chiqish versiyasi
4.1.22 / 28-mart, 2019-yil; 19 oy oldin (2019-03-28)
YozilganC ++ va GUI yilda Java
Operatsion tizimLinux
Mac OS X
Microsoft Windows
Mavjud:Ingliz tili Daniya Yapon Xitoy Litva
TuriModelni tekshirish
LitsenziyaTijorat litsenziyalari
Akademik litsenziyalar
Veb-saythttp://www.uppaal.org/ http://www.uppaal.com/

UPPAAL birlashtirilgan vosita atrof-muhit uchun modellashtirish, tekshirish va tekshirish haqiqiy vaqt tarmoqlari sifatida modellashtirilgan tizimlar vaqtli avtomatlar bilan kengaytirilgan ma'lumotlar turlari (cheklangan butun sonlar, massivlar va boshqalar).

U 1995 yilda chiqarilganidan beri kamida 17 ta amaliy ishda, shu jumladan Lego Mindstorms, uchun Flibs audio protokoli va vites qutisi boshqargichlarida Mecel.[1]

Ushbu vosita Real-Time tizimlarini loyihalashtirish va tahlil qilish guruhi tomonidan hamkorlikda ishlab chiqilgan Uppsala universiteti, Shvetsiya va Informatika bo'yicha asosiy tadqiqotlar Olborg universiteti, Daniya.

Quyidagi kengaytmalar mavjud:

  • Cora Reachability optimal narxini tahlil qilish uchun.
  • Tron On-layn real vaqt tizimlarini sinash uchun (qora quti muvofiqligini sinovdan o'tkazish).
  • Muqova COVERerage-off-layn sinovdan o'tkazish uchun maqbul.
  • Tiga TImed GAmes asosida boshqaruvchi sintezi uchun.
  • Port qisman buyurtmalarni qisqartirish usullaridan foydalangan holda komponentlarga asoslangan vaqtli tizimlar uchun.
  • Pro PRObabilistic accessability tahlil qilish uchun. (To'xtatilgan)
  • SMC Statistik modelni tekshirish uchun.

Adabiyotlar

  1. ^ "Case Studies".

Tashqi havolalar