×

zbMATH — the first resource for mathematics

\(\surd\)erics: A tool for verifying timed automata and Estelle specifications. (English) Zbl 1031.68546
Garavel, Hubert (ed.) et al., Tools and algorithms for the construction and analysis of systems. 9th international conference TACAS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2619, 278-283 (2003).
Summary: The paper presents a new tool for automated verification of Timed Automata as well as protocols written in the specification language Estelle. The current version offers an automatic translation from Estelle specifications to timed automata, and two complementary methods of reachability analysis. The first one is based on Bounded Model Checking (BMC), while the second one is an on-the-fly verification on an abstract model of the system.
For the entire collection see [Zbl 1017.00035].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
NuSMV; SPIN; Verics
PDF BibTeX XML Cite
Full Text: Link