JECDAR 0.2 - Model checking refinement relations for Timed I/O Automata
Authors
Kiviriga, Andrej ; Klicius, Napalys ; Simionescu, Cristina Ioana
Term
4. Term
Publication year
2019
Submitted on
2019-05-30
Pages
72
Abstract
Denne rapport præsenterer anden iteration af JECDAR, en Java-motor til kompositionelt design og analyse af realtidssystemer. JECDAR foreslås som et open source-alternativ til ECDAR, et eksisterende miljø, der implementerer teorien om timed input/output automata (TIOA), en formel model til at beskrive og analysere systemer, der interagerer med deres omgivelser under tidsbegrænsninger. Første version understøttede centrale operationer som refinement (forfinelse), composition (komposition) og conjunction (konjunktion). Denne iteration retter mangler for at øge korrektheden og tilføjer kontroller for determinisme, konsistens og implementering. Undervejs fandt vi flere uoverensstemmelser mellem ECDARs adfærd og den underliggende TIOA-teori; vi dokumenterer dem og anvender metoder, der hjælper vores motor med at undgå de samme faldgruber.
This report presents the second iteration of JECDAR, a Java engine for the compositional design and analysis of real-time systems. JECDAR is proposed as an open-source alternative to ECDAR, an existing environment that implements the theory of timed input/output automata (TIOA), a formal model for describing and analyzing systems that interact with their environment under timing constraints. The first version supported core operations such as refinement, composition, and conjunction. This iteration fixes shortcomings to improve correctness and adds checks for determinism, consistency, and implementation. During development, we found several mismatches between ECDAR’s behavior and the underlying TIOA theory; we document these issues and apply methods that help our engine avoid the same pitfalls.
[This abstract was generated with the help of AI]
Keywords
Documents