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
2001

Files

Résumé

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.

Détails

Titre Taxys = Esterel + Kronos: A tool for verifying real-time properties of embedded systems
Auteur(s) Bertin, Valerie ; Closse, Etienne ; Poize, Michel ; Pulou, Jacques ; Sifakis, J. ; Venier, Patrick ; Weil, D. ; Yovine, Sergio
Publié dans Proceedings of the IEEE Conference on Decision and Control
Volume 3
Pages 2875-2880
Présenté à Proceedings of the IEEE Conference on Decision and Control, Orlando, FL, United states
Date 2001
ISSN 01912216
Mots-clés (libres)
DOI https://doi.org/10.1109/CDC.2001.980712
Laboratoires RISD
Le document apparaît dans Production scientifique et compétences > I&C - Faculté Informatique & Communications > IC Archives > RISD - Laboratoire pour la conception rigoureuse des systèmes
Publications validées par des pairs
Travail hors EPFL
Papiers de conférence
Publié
Date de création de la notice 2013-03-14

PDF