ECDAR is an extension of UPPAAL TIGA for timed specifications. ECDAR and PyECDAR share the same file format for timed automata models, which allows to use the functionalities of both tools to study the same system.
PyECDAR exclusive functionalities are the followings:
- PyECDAR is a free software written in python that can be easily extended.
- Computation of parallel composition, conjunction and quotient: contrary to ECDAR, PyECDAR explicitly computes the models obtained from the compositions and allows to save them into a UPPAAL model file. This allows to see the results of these composition in ECDAR or UPPAAL GUI. In ECDAR the systems are defined in the properties and the composition are constructed on-the-fly during the analysis.
- Compatibility analysis: PyECDAR permits to check compatibility between complex components defined by composition, whereas in ECDAR since the composition are not explicit compatibility checking is only possible between atomic components.
- Robustness analyses: PyECDAR implements original algorithms for checking the robustness of timed specifications.
- Adaptive features: PyECDAR implements original algorithms for checking adaptive systems with requriements expressed in the Timed AdaCTL logic.
The following functionalities are exclusive to ECDAR:
- ECDAR Graphical User Interface is inherited from UPPAAL, a tool widely use for Timed Automata design and analysis. It allows to design Timed Input/Output Automata which forms the basics of the timed specifications theory.
- Graphical simulator: ECDAR can display the timed games strategies computed by the analyses in its graphical simulator.
