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

Studenteropgave: Kandidatspeciale og HD afgangsprojekt

  • Andrej Kiviriga
  • Napalys Klicius
  • Cristina Ioana Simionescu
4. semester, Computer Science (IT - International Track) (Kandidatuddannelse)
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.
Udgivelsesdato30 maj 2019
Antal sider72
ID: 304738440