Uppaal Model Checker
|Stable release||4.0.13 / September 27, 2010|
|Preview release||4.1.19 / July 1, 2014|
|Written in||C++ and GUI in Java|
Mac OS X
|Available in||English Danish Japanese Chinese Lithuanian|
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.).
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 for COVERerage-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.
- UPPAAL academic website
- UPPAAL commercial website
- Design and Analysis of Real-Time Systems group
- DES unit, Dept. Computer Science at AAU
|This formal methods-related article is a stub. You can help Wikipedia by expanding it.|