Untameable timed automata! (extended abstract)

Abstract

Timed automata are a widely studied model for real-time systems. Since 8 years, several tools implement this model and are successfully used to verify real-life examples. In spite of this well-established framework, we prove that the forward analysis algorithm implemented in these tools is not correct! However, we also prove that it is correct for a restricted class of timed automata, which has been sufficient for modeling numerous real-life systems. © Springer-Verlag Berlin Heidelberg 2003.