This paper presents a prototype of the
Taxys tool developed within a collaboration between France
Telecom R&D and VERIMAG. The connection of the Saxort
Esterel compiler and of the Kronos model-checker,
together with on-the-fly techniques, brings up the possibility of
verifying quantitative timing constraints on real industrial
telecommunication systems, such as a GSM radio link and a phone
prototype developed by France Telecom. In addition, Taxys
offers a non-ambiguous and user friendly formalism for specifying
quantitative timing constraints as well as high-level diagnostic
functionalities.
