UPPAAL

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
Basisdaten
Entwickler	Universität Uppsala und Universität Aalborg
Aktuelle Version	4.0.13 (27. September 2010)
Betriebssystem	Windows, Linux, macOS
Kategorie	Model Checker
Lizenz	proprietär
deutschsprachig	nein
Akademisch Kommerziell

UPPAAL gilt mittlerweile als state-of-the-art Tool und wird für vielfältige wissenschaftliche und industrielle Anwendungen eingesetzt.^[1][2]

Literatur

• Kim G. Larsen, Paul Pettersson, Wang Yi: Uppaal in a nutshell. In: International Journal on Software Tools for Technology Transfer. Nr. 1, 1997, S. 134–152.
• N. C. W. M. Braspenning, E. M. Bortnik, J. M. van de Mortel-Fronczak, J. E. Rooda: Model-based System Analysis Using Chi and Uppaal: An Industrial Case Study. In: Comput. Ind. Band 59, Nr. 1. Elsevier Science Publishers, Januar 2008, ISSN 0166-3615, S. 41–54, doi:10.1016/j.compind.2007.06.002.
• Jiansheng Xing, Bart D. Theelen, Rom Langerak, Jaco Van De Pol, Jan Tretmans, J. P. M. Voeten: UPPAAL in Practice: Quantitative Verification of a RapidIO Network. In: Proceedings of the 4th International Conference on Leveraging Applications of Formal Methods, Verification, and Validation (= ISoLA’10). Part II. Springer-Verlag, 2010, ISBN 978-3-642-16560-3, S. 160–174.
• Timothy Bourke, Arcot Sowmya: Analyzing an Embedded Sensor with Timed Automata in Uppaal. In: ACM (Hrsg.): ACM Trans. Embed. Comput. Syst. Band 13, Nr. 3, Dezember 2013, S. 44:1–44:26, doi:10.1145/2539036.2539040.

Weblinks

• Website akademische Anwendungen
• Website für kommerzielle Anwendungen

Einzelnachweise

1. Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. Nasa Technical Reports Server, Bibliogov, 2013, ISBN 978-1-289-28314-8
2. Stephan 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.