zbMATH — the first resource for mathematics

TAXYS: A tool for the development and verification of real-time embedded systems. (English) Zbl 0991.68644
Berry, GĂ©rard (ed.) et al., Computer aided verification. 13th international conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2102, 391-395 (2001).
Summary: 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 real-time 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 the 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 sessions.
For the entire collection see [Zbl 0969.00081].

68U99 Computing methodologies and applications
68Q60 Specification and verification (program logics, model checking, etc.)
Kronos; TAXYS; PVS
Full Text: Link