Editing Uppaal Model Checker

{{Short description|Integrated tool environment}}
{{Infobox software
| name                   = UPPAAL
| logo                   = 
| screenshot             = 
| caption                = 
| developer              = [[Uppsala University]]<br/>[[Aalborg University]]
| released               = {{Start date|1995}}
| latest release version =  5.0.0
| latest release date    = {{release date and age|2023|07|14}}
| latest preview version =  5.1.0-beta3
| latest preview date    = {{release date and age|2023|10|23}}
| programming_language   = [[C++]] and [[GUI]] in [[Java (programming language)|Java]]
| operating system       = [[Linux]]<br/>[[Mac OS X]]<br/>[[Microsoft Windows]]
| platform               = 
| genre                  = [[Model checking]]
| language               = [[English language|English]] [[Danish language|Danish]] [[Japanese language|Japanese]] [[Chinese language|Chinese]] [[Lithuanian language|Lithuanian]]
| license                = [[Commercial Licenses]]<br/>[[Academic Licenses]]
| website                = http://www.uppaal.org/ http://www.uppaal.com/
}}
'''UPPAAL''' is an integrated [[tool]] [[software platform|environment]] for [[model checking|modeling]], validation and verification of [[real-time computing|real-time]] systems modeled as networks of [[timed automaton|timed automata]], extended with [[data type]]s (bounded integers, arrays etc.).

It has been used in at least 17 case studies since its release in 1995, including on [[Lego Mindstorms]], for the [[Philips]] audio protocol, and in gearbox controllers for [[Mecel]].<ref>{{cite web|url=http://www.it.uu.se/research/group/darts/uppaal/examples.shtml|title=Case Studies}}</ref>

The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at [[Uppsala University]], [[Sweden]] and Basic Research in Computer Science at [[Aalborg University]], [[Denmark]].

There are the following extensions available:
*'''[http://people.cs.aau.dk/~adavid/cora/ Cora]''' for Cost Optimal Reachability Analysis.
*'''[http://people.cs.aau.dk/~marius/tron/ Tron]''' for Testing Real-time systems ON-line (black-box conformance testing).
*'''[http://user.it.uu.se/~hessel/CoVer/ Cover]''' for COVERerage-optimal off-line test generation.
*'''[http://people.cs.aau.dk/~adavid/tiga/ Tiga]''' for TImed GAmes based controller synthesis.
*'''[http://www.it.uu.se/research/group/darts/uppaal/port/ Port]''' for component based timed systems, exploiting Partial Order Reduction Techniques.
*'''Pro''' for PRObabilistic reachability analysis. (Discontinued)
*'''[http://people.cs.aau.dk/~adavid/smc/ SMC]''' for Statistical Model Checking.

==References==
{{Reflist}}

==External links==
*[http://www.uppaal.org/ UPPAAL academic website]
*[http://www.uppaal.com/ UPPAAL commercial website]
*[http://www.it.uu.se/research/group/darts/ Design and Analysis of Real-Time Systems group] 
*[http://www.cs.aau.dk/research/distributed-embedded-intelligent-systems/ DEIS unit, Dept. Computer Science at AAU]

[[Category:Model checkers]]


{{formalmethods-stub}}