Uppaal Model Checker
Developer(s) |
Uppsala University Aalborg University |
---|---|
Initial release | 1995 |
Stable release |
4.0.13
/ September 27, 2010 |
Preview release |
4.1.19
/ July 1, 2014 |
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.).
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. (Discontinued)
- SMC for Statistical Model Checking.
External links
- UPPAAL academic website
- UPPAAL commercial website
- Design and Analysis of Real-Time Systems group
- DEIS unit, Dept. Computer Science at AAU
This article is issued from Wikipedia - version of the 9/6/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.