Harman Patil (Editor)

Uppaal Model Checker

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit
Initial release
  
1995 (1995)

Written in
  
C++ and GUI in Java

Developer(s)
  
Uppsala University Aalborg University

Stable release
  
4.0.13 / September 27, 2010; 6 years ago (2010-09-27)

Preview release
  
4.1.19 / July 1, 2014; 2 years ago (2014-07-01)

Operating system
  
Linux Mac OS X Microsoft Windows

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.

    • References

    Uppaal Model Checker Wikipedia
    (Text) CC BY-SA