A master thesis from Aalborg University
Compositional Backwards Reachability of Timed Automata
Author(s)
Term
4. term
Education
Publication year
2002
Submitted on
2012-02-14
Abstract
This report deals with the development of a general framework for Compositional Backwards Reachability (CBR) and with the verification of reachability properties on Timed Automata Networks (TAN). The CBR method is developed on the basis of a series of finer and finer partitionings of the state-space. Two different CBR algorithms are presented and proven correct. The domain of TAN, which is a real-time model, is described. The symbolic DBM-based analysis of Timed Automata used in existing verification tools, like Uppaal is explained. The second of the CBR algorithms is applied to the domain of TAN. Several extensions to the domain are discussed, and a test implementation of the basic method is developed. This implementation is used to obtain some experimental results. Finally future work is discussed and a conclusion is drawn.
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.