TAXYS : a Tool for Developing and Verifying Real-Time Properties of Embedded Systems

Daniel Weil, Etienne Closse, Michel Poize, Patrick Venier and Jacques Pulou (France Telecom R&D), Sergio Yovine and Joseph Sifakis (VERIMAG)

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems