JECDAR 0.2 - Model checking refinement relations for Timed I/O Automata
Term
4. Term
Publication year
2019
Submitted on
2019-05-30
Pages
72
Abstract
This report documents the continuation of the work done in order to implement the second iteration of JECDAR, or a Java Engine for Compositional Design and Analysis of Real Time Systems. This tool is proposed as an open-source alternative to ECDAR, an already existing environment that implements the theory of timed input/output automata, which is what JECDAR does as well. While the first version of JECDAR contained features like refinement, composition and conjunction, this version addresses various shortcomings in an attempt to reach correctness. Moreover, it adds features such as a determinism, consistency and implementation check. In the process, several inconsistencies between ECDAR and the theory of timed input/output automata were discovered. We document them and employ various methods to ensure our engine avoids such pitfalls.
Keywords
Documents