A master thesis from Aalborg University
Concrete Delays for Symbolic Traces
[Konkrete Tidsværdier for Symbolske Eksekveringer]
Author(s)
Term
2. term
Education
Publication year
2010
Submitted on
2010-05-31
Pages
87 pages
Abstract
The goal of model checking is verifying that a system adheres to its specification. The model checking tool UPPAAL verifies Timed Automata and returns diagnostic traces to help users understand violations of the specifications. Due to the time abstractions used in the computations, the diagnostic traces returned are hard to comprehend for users, as they do not contain concrete delays. In this thesis we describe several approaches to generating concrete delays for diagnostic traces. Two of these approaches are based on the diagnostic traces that violate safety properties and one approach is based on the diagnostic traces that violate liveness properties. We prove the correctness of all approaches and test the safety approaches against each other. The liveness approach is tested for viability.
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.