A master thesis from Aalborg University
JECDAR 0.2 - Model checking refinement relations for Timed I/O Automata
Author(s)
Term
4. Term
Publication year
2019
Submitted on
2019-05-30
Pages
72 pages
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
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.