zbMATH — the first resource for mathematics

Diagonal constraints in timed automata: Forward analysis of timed systems. (English) Zbl 1175.68256
Pettersson, Paul (ed.) et al., Formal modeling and analysis of timed systems. Third international conference, FORMATS 2005, Uppsala, Sweden, September 26–28, 2005. Proceedings. Berlin: Springer (ISBN 3-540-30946-2/pbk). Lecture Notes in Computer Science 3829, 112-126 (2005).
Summary: Timed automata (TA) are a widely used model for real-time systems. Several tools are dedicated to this model, and they mostly implement a forward analysis for checking reachability properties. Though diagonal constraints do not add expressive power to classical TA, the standard forward analysis algorithm is not correct for this model. In this paper we survey several approaches to handle diagonal constraints and propose a refinement-based method for patching the usual algorithm: erroneous traces found by the classical algorithm are analyzed, and used for refining the model.
For the entire collection see [Zbl 1097.68008].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Full Text: DOI