UPPAAL

from Wikipedia, the free encyclopedia
UPPAAL
Basic data

developer Uppsala University and Aalborg University
Current  version 4.0.13
(September 27, 2010)
operating system Windows , Linux , macOS
category Model checker
License proprietary
German speaking No
Academically Commercial

UPPAAL is a model checker that is being developed at Uppsala University and Aalborg University . UPPAAL is available free of charge for academic purposes. In contrast to other model checkers such as SPIN or Rebeca , the system is not mainly modeled using a formal language in text form, but rather using a graphic editor. The individual states and the transitions between them are displayed in this graphic editor. Local and global variables as well as individual functions are specified in a C -like language. Properties to be checked are formulated with LTL . License fees are charged for commercial use. UPPAAL is often used in the verification of algorithms for embedded systems.

UPPAAL is now considered a state-of-the-art tool and is used for a variety of scientific and industrial applications.

literature

  • Kim G. Larsen, Paul Pettersson, Wang Yi: Uppaal in a nutshell . In: International Journal on Software Tools for Technology Transfer . No. 1 , 1997, p. 134-152 .
  • NCWM Braspenning, EM Bortnik, JM van de Mortel-Fronczak, JE Rooda: Model-based System Analysis Using Chi and Uppaal: An Industrial Case Study . In: Comput. Ind. Band 59 , no. 1 . Elsevier Science Publishers, January 2008, ISSN  0166-3615 , p. 41-54 , doi : 10.1016 / j.compind.2007.06.002 .
  • Jiansheng Xing, Bart D. Theelen, Rom Langerak, Jaco Van De Pol, Jan Tretmans, JPM 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 , pp. 160-174 .
  • Timothy Bourke, Arcot Sowmya: Analyzing an Embedded Sensor with Timed Automata in Uppaal . In: ACM (Ed.): ACM Trans. Embed. Comput. Syst. tape 13 , no. 3 , December 2013, p. 44: 1-44: 26 , doi : 10.1145 / 2539036.2539040 .

Web links

Individual evidence

  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: Formal models of software development: model checking, verification, analysis and simulation. Springer-Verlag, 2009, ISBN 978-3-8348-0669-7 . Here: Chapter 3: Model checking with Timed automata and Uppaal , p. 117 ff.