Taxys = Esterel + Kronos: A tool for verifying real-time properties of embedded systems
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.
Keywords: Algorithms ; Approximation theory ; C (programming language) ; Computational complexity ; Computer graphics ; Computer hardware ; Program processors ; Real time systems ; Software prototyping ; Telecommunication systems ; Voice/data communication systems
Record created on 2013-03-14, modified on 2016-08-09