Title :
TAXYS=Esterel+Kronos. A tool for verifying real-time properties of embedded systems
Author :
Bertin, V. ; Closse, E. ; Poize, M. ; Pulou, J. ; Sifakis, J. ; Venier, P. ; Weil, D. ; Yovine, S.
Author_Institution :
Central R&D, ST Microelectron., Crolles, France
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 to real industrial telecommunication systems, such as a GSM radio link from Alcatel and a phone prototype from France Telecom
Keywords :
ISDN; cellular radio; embedded systems; formal verification; program compilers; software engineering; telecommunication computing; Alcatel; ESTEREL compiler; France Telecom; GSM radio link; ISDN phone prototype; KRONOS; SAXO-RT; TAXYS; embedded codes; formal verification; real-time systems; schedulability; telecommunication systems; timed model; Automatic control; Control system synthesis; Embedded system; Force control; Job shop scheduling; Real time systems; Research and development; Runtime; Telecommunications; Timing;
Conference_Titel :
Decision and Control, 2001. Proceedings of the 40th IEEE Conference on
Conference_Location :
Orlando, FL
Print_ISBN :
0-7803-7061-9
DOI :
10.1109/.2001.980712
