Uppaal Model Checker - Uppaal Model Checker

UPPAAL
VývojářiUniverzita v Uppsale
Aalborg University
První vydání1995 (1995)
Stabilní uvolnění
4.0.14 / 20. května 2014; před 6 lety (2014-05-20)
Náhled verze
4.1.22 / 28. března 2019; Před 19 měsíci (2019-03-28)
NapsánoC ++ a GUI v Jáva
Operační systémLinux
Mac OS X
Microsoft Windows
K dispozici vAngličtina dánština japonský čínština Litevský
TypKontrola modelu
LicenceObchodní licence
Akademické licence
webová stránkahttp://www.uppaal.org/ http://www.uppaal.com/

UPPAAL je integrovaný nářadí životní prostředí pro modelování, ověřování a ověřování reálný čas systémy modelované jako sítě časované automaty, rozšířené o typy dat (ohraničená celá čísla, pole atd.).

Od svého vydání v roce 1995 byl použit v nejméně 17 případových studiích, včetně Lego Mindstorms, pro Philips audio protokol a v řadičích převodovky pro Mecel.[1]

Tento nástroj byl vyvinut ve spolupráci mezi skupinou Design and Analysis of Real-Time Systems ve společnosti Univerzita v Uppsale, Švédsko a základní výzkum v informatice na Aalborg University, Dánsko.

K dispozici jsou následující rozšíření:

  • Cora pro analýzu nákladové optimální dosažitelnosti.
  • Tron pro testování ON-line systémů v reálném čase (testování shody černé skříňky).
  • Pokrýt pro generování off-line testů COVERerage.
  • Tiga pro syntézu řadičů založených na TImed GAmes.
  • Přístav pro časované systémy založené na komponentách využívající techniky částečné redukce objednávek.
  • Pro pro analýzu pravděpodobnostní dostupnosti. (Ukončeno)
  • SMC pro kontrolu statistického modelu.

Reference

  1. ^ "Případové studie".

externí odkazy