UPPAAL
| UPPAAL | |
|---|---|
| Basisdaten
| |
| Entwickler | Universität Uppsala und Universität Aalborg |
| Aktuelle Version | 4.0.13 (27. September 2010) |
| Betriebssystem | Windows, Linux, Mac OS X |
| Kategorie | Model Checker |
| Lizenz | proprietär |
| deutschsprachig | nein |
| Akademisch Kommerziell | |
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.[1][2]
Weblinks
Literatur
- Larsen, Kim G. and Pettersson, Paul and Yi, Wang: Uppaal in a nutshell. In: International Journal on Software Tools for Technology Transfer (= 1). 1997, S. 134–152.
- Braspenning, N. C. W. M. and Bortnik, E. M. and van de Mortel-Fronczak, J. M. and Rooda, J. E.: Model-based System Analysis Using Chi and Uppaal: An Industrial Case Study. In: Elsevier Science Publishers B. V. (Hrsg.): Comput. Ind. Band 59, Nr. 1, Januar 2008, ISSN 0166-3615, S. 41--54, doi:10.1016/j.compind.2007.06.002.
- Xing, Jiansheng and Theelen, Bart D. and Langerak, Rom and Van De Pol, Jaco and Tretmans, Jan and Voeten, J. P. M.: UPPAAL in Practice: Quantitative Verification of a RapidIO Network. In: Springer-Verlag (Hrsg.): Proceedings of the 4th International Conference on Leveraging Applications of Formal Methods, Verification, and Validation - Volume Part II (= ISoLA'10). 2010, ISBN 978-3-642-16560-3, S. 160--174.
- Bourke, Timothy and Sowmya, Arcot: 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.
Einzelnachweise
- ↑ Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal., Nasa Technical Reports Server, Bibliogov, 2013, ISBN 978-1289283148
- ↑ Stephan Kleuker: Formale Modelle der Softwareentwicklung: Model-Checking, Verifikation, Analyse und Simulation. Hier: Kapitel 3: Modelchecking mit Timed automata und Uppaal, Springer-Verlag, 2009, S. 117 ff. ISBN 978-3834806697