This page describes the Ecdar tool architecture as of spring 2022.
The general design intent of having two verification engines, is that it should make the whole platform more reliable.
j-Ecdar
The intention of j-Ecdar is to be a form of reference implementation, where no effort is put into optimizing the code for speed, but rather for
- Correctness
- Readability
Reveaal
The intention of the Reveaal engine is to get a verification engine that is fast and parallelizable. Both over multiple cores, but also in the long run over multiple machines. The design goals for Reveaal are
- Correctness
- Speed
- Remove dependency to UDBM
Ecdar GUI
The intention of the GUI is be quick and usable to create and edit models. It should provide visual feedback on the verification.
- Visualization of zones
- Visualization of refinement relations
- Integration with revision control (Git)
Test framework
Automated test of the two engines. This component is vital in order allow to obtain the ability to actually refactor code in the engines with confidence.
- Hand designed test cases with known results
- Conformance testing between the two engines
- Automated performance testing