JECDAR 0.2 - Model checking refinement relations for Timed I/O Automata

Student thesis: Master thesis (including HD thesis)

  • Andrej Kiviriga
  • Napalys Klicius
  • Cristina Ioana Simionescu
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.
LanguageEnglish
Publication date30 May 2019
Number of pages72
ID: 304738440