Fig 1 (click for a larger view).
ECDAR is a tool implementing the timed interface theory of [DLLNW10]. Its architecture reuses parts of UPPAAL. The tool itself is the fruit of the collaboration between Aalborg University, INRIA (Axel Legay), and ITU (Andrzej Wasowski).
The input language is timed I/O automata and is defined using, respectively, the modalities controllable and uncontrollable to define, respectively, inputs and outputs. ECDAR treats timed game automata as timed I/O automata and opens the way to incremental design and compositional reasoning.
The tool is designed to check incrementally refinement between specifications. As shown in Fig. 1, it is possible to combine different timed I/O automata with the composition or conjunction operators and check if the combined specification refines another specification (that can be defined with such operators as well).
- [DLLNW10] Alexandre David, Kim.G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. Timed I/O automata: a complete specification theory for real-time systems. Accepted for HSCC 2010, to appear.
Latest NewsTiga version 0.17 released.
27 Mar 2014
Tiga 0.17 now includes Ecdar.Version 0.10 released.
13 Apr 2013
Bug fix release. IO specifications are now explicit and must be defined after the system declaration. See the updated examples for the intuitive syntax. A 64-bit version for the command line verifier has been added - do not use any option that uses CDDs, do not use interactive play.Version 0.9 for Mac released.
21 Oct 2010
The Mac version of ECDAR is now available, courtesy of Didier Lime.Version 0.9 released.
14 Oct 2010
A new version of ECDAR is released today. This version fixes numerous problems related to the simulator and the checker.Version 0.8 released.
7 May 2010
A new version of ECDAR is released today. This version fixes a crash in the server when no strategy is available and the simulator is used anyway.Version 0.7 released.
5 May 2010
A new version of ECDAR is released today. This version improves the simulator and has a better support for the quotient.ECDAR new homepage.
12 Apr 2010
ECDAR has now a new homepage.ECDAR pre-release 0.6.
9 Apr 2010
A new version of ECDAR is released today. This version improves the simulator and fixes some bugs related accepted models for the refinement checker. The simulator works better for simulating refinement strategies.