UPPAAL

UPPAAL ist eine integrierte Werkzeugumgebung für die Modellierung, Validierung und Verifikation von Echtzeitsystemen, wie Netzwerke von Zeitautomaten, erweiterbar um Datentypen (Ganzzahlen begrenzt, Arrays, etc.) modelliert.
UPPAAL CORA ist ein Zweig der UPPAAL für Kosten Optimale Erreichbarkeit Anslysis vom UPPAAL Team als Teil der VHS und AMETIST Projekte entwickelt. Wohingegen UPPAAL unterstützt Model Checking von Zeitautomaten verwendet UPPAAL CORA eine Verlängerung des Zeitautomaten genannt LPTA. LPTA können Sie das Modell mit dem Begriff der Kosten zu kommentieren.
Dies kann die Kosten für die Verzögerung in bestimmten Situationen oder die Kosten für bestimmte Aktionen sein. UPPAAL CORA findet dann optimale Pfade passenden Zielbedingungen.
UPPAAL CORA hat in einer Reihe von Fallstudien verwendet. Einige davon werden auf der Fallstudie Seite dieser Website beschrieben. Wenn Sie kommen mit interessanten Anwendungen, kontaktieren Sie uns bitte. Wir sind daran interessiert zu hören, was Sie tun!
Wegen der unterschiedlichen internen Datenstrukturen, besteht derzeit aus zwei verschiedenen Versionen UPPAAL CORA:
Eine Version für den vereinfachten Fall der Zeit optimal Erreichbarkeitsanalyse.
Eine Version für die volle Sprache LPTA.
Wie UPPAAL ist UPPAAL CORA kostenlos für nicht-kommerziellen Gebrauch, zB für die Bewertung, Forschung und Lehrzwecke.
Hier sind einige der wichtigsten Features von "UPPAAL":
Robust
 
· Die Modellierungssprache von UPPAAL CORA ist robust gegenüber Veränderungen in der Problem modelliert. Dies bedeutet, dass Ihre Investition in die Modellierung ist nicht verloren, wenn das Problem verändert, da es einfach ist, das bestehende Modell anzupassen.
 
Schnell
 
· Auch wenn die Technologie ist nicht neu, experimenteller und sehr verschieden von Techniken, die in der traditionellen Unternehmensforschung verwendet wird, ist UPPAAL CORA in einer Reihe von Fallstudien wettbewerbsfähig.
 
Kompatibel
 
· Die Sprache der UPPAAL CORA ist eine Obermenge UPPAAL. Jeder gültige UPPAAL Modell ist auch ein gültiger UPPAAL CORA Modell. Dies macht es einfach und bequem zu Wiederverwendung und Ihre bestehende Modelle passen sich CORA Uppaal.
 
Strom
 
· UPPAAL CORA basiert auf der neuesten Version von internen Entwicklungs UPPAAL basiert, enthält die neuesten Leistungsverbesserungen und Sprache. Es ist jedoch ein Versuchswerkzeug und fehlen viele der Verifizierungsmerkmale UPPAAL.
Einschränkungen:
UPPAAL CORA mit voller LPTA Träger eine Reihe von Einschränkungen. Diese Beschränkungen sind nicht fundamental, sondern sind das Ergebnis der Verwendung von neuen internen Datenstrukturen mit einem derzeit beschränkt Feature-Set. Mit der Zeit werden diese Einschränkungen gelöst werden.
- Keine Extrapolation, daher Kündigung ist nicht gewährleistet, wenn Sie garantieren, dass entweder:
· Das System ist azyklisch.
· Alle Uhren werden von Invarianten begrenzt.
- Einfache Erreichbarkeit nur:
· Kein Verfügbarkeitsprüfung
· Kein Deadlock-Prüfung
- Eingeschränkte Verwendung von Führung:
· Unterstützung für (Kosten + Rest) Sortierung wird umgesetzt (best first search)
· Unterstützung für heuristische Variable implementiert ist, sondern der Ausdruck ist nicht auf die Kosten Variable.
Was ist neu in dieser Version:
· Diese Version behebt Crash Bugs und einen Speicherverlust.