Taxys = Esterel + Kronos: A tool for verifying real-time properties of embedded systems
- Bertin, Valerie
- Closse, Etienne
- Poize, Michel
- Pulou, Jacques
- Sifakis, J.
- Venier, Patrick
- Weil, D.
- Yovine, Sergio
Publication date
March 2013
DOI Publisher
Institute of Electrical and Electronics Engineers (IEEE)Abstract
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 on real industrial telecommunication systems, such as a GSM radio link from Alcatel and a phone prototype from France Telecom
Add to ORKG