History

This is a short outline of the history of the development of the different parts of the Ecdar tools.

Uppaal TIGA versions  - 2010 - 2013

The first version of the tool (0.6 to 0.10) (http://people.cs.aau.dk/~adavid/ecdar/ - defunct webpage) was based on the GUI and verification engine of Uppaal TIGA. Efter this it was released as part of Uppaal TIGA in version 0.17.

These versions all had the problem that the GUI was designed for the Uppaal TIGA semantics and thus did not match the Ecdar Timed Input/Output Automata (TIOA) semantics. This version also inherited most of the extension of Timed Automata (TA), including a lot of features that did not have defined semantics in the associated papers. Uses the .xml file format.

PyEcdar - 2013

PyEcdar was a partial implementation of the TIOA semantics implemented by Louis-Marie Traonouez while at INRIA in France. As the name suggests this version was implemented in Python. It was built using the Uppaal Difference Bound Matrix (UDBM) library, which is licensed under GPL 2.0.  Uses the .xml file format.

  • In 2020 Florian Lorber managed to make the source code compile, but on closer inspection certain important features that we assumed where implemented were not actually implemented in the code base.

Ecdar GUI - 2017

The Ecdar GUI is built on the H-Uppaal GUI that was developed the year before. This GUI is written in JavaFX and is the base for the current version of the Ecdar GUI (github). Uses the .json file format as introduced by H-Uppaal.

This version contained a simulator that linked with the old Ecdar TIGA based verification engine. And a mutation based conformance testing tool.

Simultaneously a tool for visualizing zones in three dimensions was developed, but not integrated with the other tools.

j-Ecdar - 2018

Implementation of part of the TIOA theory in Java (JECDAR 0.2.pdf), also using the UDBM library. Can input and output both .json and .xml file formats.

As of the spring of 2021 this code is being worked on to make it feature complete and enable research based on this tool. (j-Ecdar on github)

Reveaal - 2020

An implementation in Rust of the same features as the j-Ecdar engine. This code base also uses the UDBM library. Based on the tool HMKaal that was also written in Rust, but used a different semantics of the models.