Uppaal Model Checker

UPPAAL

Utvecklare	Uppsala universitet Ålborg universitet
Initial release	1995 ( 1995 )
Stabil frisättning	4.0.14 / 20 maj 2014 ( 2014-05-20 )
Förhandsgranska release	4.1.22 / 28 mars 2019 ( 2019-03-28 )
Skrivet i	C++ och GUI i Java
Operativ system	Linux Mac OS X Microsoft Windows
Tillgänglig i	Engelska danska japanska kinesiska litauiska
Typ	Modellkontroll
Licens	Kommersiella licenser Akademiska licenser
Hemsida	http://www.uppaal.org/ http://www.uppaal.com/

UPPAAL är en integrerad verktygsmiljö för modellering , validering och verifiering av realtidssystem modellerade som nätverk av tidsstyrda automater , utökat med datatyper (begränsade heltal, arrayer etc.).

Den har använts i minst 17 fallstudier sedan den släpptes 1995, inklusive på Lego Mindstorms , för Philips ljudprotokoll och i växellådskontroller för Mecel .

Verktyget har utvecklats i samarbete mellan Design and Analysis of Real-Time Systems-gruppen vid Uppsala universitet , Sverige och Grundforskning i datavetenskap vid Aalborg Universitet , Danmark .

Det finns följande tillägg tillgängliga:

• Cora för kostnadsoptimal nåbarhetsanalys.
• Tron för testning av realtidssystem ON-line (testning av överensstämmelse med svart låda).
• Cover för COVERerage-optimal off-line testgenerering.
• Tiga för TImed GAmes-baserad kontrollsyntes.
• Port för komponentbaserade tidsinställda system, med hjälp av partiell orderreduktionsteknik.
• Pro för PRObabilistisk nåbarhetsanalys. (upphört)
• SMC för statistisk modellkontroll.

externa länkar

• UPPAAL akademiska webbplats
• UPPAAL kommersiell webbplats
• Design och analys av Real-Time Systems grupp
• DEIS-enheten, Inst. datavetenskap vid AAU