TAXYS: a tool for the development and verification of real-time embedded systems

The correct behavior of real-time applications depends not only on the correctness of the results of computations but also on the times at which these results are produced. As a matter of fact, violations of real-time constraints in embedded systems are the most difficult errors to detect, because they are extremely sensitive both to the patterns of external events stimulating the system and to the timing behavior of the system itself. Clearly, the development of realtime systems requires rigorous methods and tools to reduce development costs and "time-to-market" while guaranteeing the quality of the produced code (in particular, respect of the temporal constraints). The above requirements motivated the development of the TAXYS tool, dedicated to the design and validation of real-time telecommunications software. One of the major goal of the TAXYS tool is to produce a formal model that captures the temporal behavior of the whole application which is composed of the embedded computer and its external environment. For this purpose we use the formal model of timed automata. The choice of this model allows the use of results, algorithms and tools available. Here, we use the KRONOS model checker for model analysis. From the source code of the application, an ESTEREL program annotated with temporal constraints, the TAXYS tool produces on one hand a sequential executable code and on the other hand a timed model of the application. This model is again composed with a timed model of the external environment in order to obtain a global model which is statically analyzed to validate timing constraints. This validation should notably shorten design time by limiting tedious test and simulation session