Predictability of a RTX2000-based implementation

Any implementation should be proven to meet its specification. In this paper, we cope with the issue of checking the temporal correctness of a real-time program, implemented on a RTX microcontroller. Our real-time programs are first written in a high-level synchronous language (Esterel). and then, automatically translated into T-forth. Under these assumptions, the temporal behaviour of the generated RTX program can be predicted, at compile-time. In this paper, we present algorithms that compute realistic durations of system reactions. These algorithms use an abstract representation of the RTX program based on a behavioural semantics given to T-forth.