Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
UPPAAL CORA
[go: Go Back, main page]
Skip to main content.

Welcome!

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.).

UPPAAL CORA is a branch of UPPAAL for Cost Optimal Reachability Anslysis developed by the UPPAAL team as part of the VHS and AMETIST projects. Whereas UPPAAL supports model checking of timed automata, UPPAAL CORA uses an extension of timed automata called LPTA. LPTA allows you to annotate the model with the notion of cost. This can be the cost of delay in certain situations or the cost of particular actions. UPPAAL CORA then finds optimal paths matching goal conditions.

UPPAAL CORA has been used in a number of case studies. Some of these are described on the case study page of this site. If you come up with interesting uses, please contact us. We are interested in hearing what you do!

Due to different internal data structures, UPPAAL CORA currently consists of two different versions:

  • A version for the simplified case of time optimal reachability analysis.
  • A version for the full language of LPTA.

Like UPPAAL, UPPAAL CORA is free for non-profit use, e.g. for evaluation, research, and teaching purposes.

Latest News

UPPAAL Got New Home Page

25 Jan 2005

The main UPPAAL site adopted the same layout as the UPPAAL CORA site. At the same time, the UPPAAL CORA site has adopted a new color scheme.

Updated case studies

30 Nov 2004

The models of the case studies can now be downloaded from the case study page.

More News »

Robustness

The modeling language of UPPAAL CORA is robust towards changes in the problem modeled. This means that your investment in modeling is not lost when the problem changes, since it is easy to adapt the existing model.

Performance

Although the technology is rather new, experimental and very different from techniques used in traditional operational research, UPPAAL CORA is competitive in a number of case studies.

Compatibility

The language of UPPAAL CORA is a superset of UPPAAL. Any valid UPPAAL model is also a valid UPPAAL CORA model. This makes it easy and convenient to reuse and adapt your existing models to UPPAAL CORA.

Current

UPPAAL CORA is based on the latest internal development version of UPPAAL, containing the latest performance and language improvements. It is however an experimental tool and lacks many of the verification features of UPPAAL.