UPPAAL ist ein Model Checker, der an der Universität Uppsala und der Universität Aalborg entwickelt wird. UPPAAL steht für akademische Zwecke kostenlos zur Verfügung. Im Gegensatz zu anderen Model Checkern wie SPIN oder Rebeca erfolgt die Modellierung des Systems nicht hauptsächlich über eine formale Sprache in Textform, sondern durch einen grafischen Editor. In diesem grafischen Editor werden die einzelnen Zustände und die Übergänge zwischen diesen dargestellt. Lokale und globale Variablen sowie einzelne Funktionen werden in einer C-ähnlichen Sprache spezifiziert. Zu überprüfende Eigenschaften werden mit LTL formuliert. Bei kommerzieller Anwendung werden Lizenzgebühren erhoben. UPPAAL wird häufig in der Überprüfung von Algorithmen für Embedded-Systems verwendet.
UPPAAL gilt mittlerweile als state-of-the-art Tool und wird für vielfältige wissenschaftliche und industrielle Anwendungen eingesetzt.Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. Nasa Technical Reports Server, Bibliogov, 2013, ISBN 978-1-289-28314-8Stephan Kleuker: Formale Modelle der Softwareentwicklung: Model-Checking, Verifikation, Analyse und Simulation. Springer-Verlag, 2009, ISBN 978-3-8348-0669-7. Hier: Kapitel 3: Modelchecking mit Timed automata und Uppaal, S. 117 ff.
Literatur
Weblinks Website akademische Anwendungen Website für kommerzielle Anwendungen
Einzelnachweise
Kategorie:Beschreibungssprache Kategorie:Automatentheorie Kategorie:Theoretische Informatik Kategorie:Abkürzung