This article may rely excessively on sources too closely associated with the subject, potentially preventing the article from being verifiable and neutral. Please help improve it by replacing them with more appropriate citations to reliable, independent sources. (June 2025) (Learn how and when to remove this message) |
| UPPAAL | |
|---|---|
| Developers | Uppsala University Aalborg University |
| Release | 1995 (1995) |
| Stable release | 5.0.0
/ July 14, 2023; 2 years ago (2023-07-14) |
| Preview release | 5.1.0-beta3
/ October 23, 2023; 2 years ago (2023-10-23) |
| Written in | C++ and GUI in Java |
| Operating system | Linux Mac OS X Microsoft Windows |
| Available in | English Danish Japanese Chinese Lithuanian |
| Type | Model checking |
| License | Commercial Licenses Academic Licenses |
| Website | http://www.uppaal.org/ http://www.uppaal.com/ |
UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (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.[1]
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:
- Cora for Cost Optimal Reachability Analysis.
- Tron for Testing Real-time systems ON-line (black-box conformance testing).
- Cover Archived 2021-01-17 at the Wayback Machine for COVERage-optimal off-line test generation.
- Tiga for TImed GAmes based controller synthesis.
- Port for component based timed systems, exploiting Partial Order Reduction Techniques.
- Pro for PRObabilistic reachability analysis. (Discontinued)
- SMC for Statistical Model Checking.
References
[edit]External links
[edit]- UPPAAL academic website
- UPPAAL commercial website
- Design and Analysis of Real-Time Systems group
- DEIS unit, Dept. Computer Science at AAU
