UPPAAL is an integrated
tool environment
Environment most often refers to:
__NOTOC__
* Natural environment, all living and non-living things occurring naturally
* Biophysical environment, the physical and biological factors along with their chemical interactions that affect an organism or ...
for
modeling, validation and verification of
real-time systems modeled as networks of
timed automata In automata theory, a timed automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can ...
, extended with
data type
In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allowed operations on it. A data type tells the compiler or interpreter how the programmer intends to use the data. Most progra ...
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
Mecel is a software and systems consulting firm, specializing in the automotive industry. The company has offices in Gothenburg and has approximately 120 employees.
History
Mecel was founded in Sweden in 1982 by Jan Nytomt and Hasse Johansson, ...
.
The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at
Uppsala University,
Sweden
Sweden, formally the Kingdom of Sweden,The United Nations Group of Experts on Geographical Names states that the country's formal name is the Kingdom of SwedenUNGEGN World Geographical Names, Sweden./ref> is a Nordic country located on ...
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
External links
UPPAAL academic websiteUPPAAL commercial websiteDesign and Analysis of Real-Time Systems group
DEIS unit, Dept. Computer Science at AAU
Model checkers
{{formalmethods-stub