TAXYS=Esterel+Kronos. A tool for verifying real-time properties of embedded systems
Valérie Bertin, Etienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis, Patrick Venier, Daniel Weil, Sergio Yovine · Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No.01CH37228) · 2003
The goal of TAXYS is to provide a framework for developing real-time embedded code and verifying its correct behavior with respect to quantitative timing requirements. To achieve so, TAXYS connects France Telecom's ESTEREL compiler SAXO-RT with VERIMAG's model-checker KRONOS. TAXYS has been successfully applied to real industrial telecommunication systems, such as a GSM radio link from Alcatel and a phone prototype from France Telecom.