© University of Kent - Contact | Feedback | Legal | FOI | Cookies
A tool for the syntactic detection of zeno-timelocks in timed automata
H Bowman, R Gomez, and L Su
Electronic Notes in Theoretical Computer Science, 139(1):182-196, November 2005 Proceedings of the 6th AMAST Workshop on Real-time Systems (ARTS 2004).Abstract
Timed automata are a very successful notation for specifying and verifying real-time systems, but timelocks can freely arise. These are counter-intuitive situations in which a specifier's description of a component automaton can inadvertently prevent time from passing beyond a certain point, possibly making the entire system stop. In particular, a zeno-timelock represents a situation where infinite computation is performed in a finite period of time. Zeno-timelocks are very hard to detect for real-time model checkers, e.g. UPPAAL and Kronos. We have developed a tool which can take an UPPAAL model as input and return a number of loops which can potentially cause zeno-timelocks. This tool implements an algorithm which refines a static verification approach introduced by Tripakis. We illustrate the use of this tool on a real-life case-study, the CSMA/CD protocol.
Download publication 216 kbytesBibtex Record
@article{2269, author = {H Bowman and R Gomez and L Su}, title = {{A tool for the syntactic detection of zeno-timelocks in timed automata}}, month = {November}, year = {2005}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {Proceedings of the 6th AMAST Workshop on Real-time Systems (ARTS 2004)}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/2005/2269}, publication_type = {article}, submission_id = {21621_1131013767}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {139}, number = {1}, publisher = {Elsevier}, }