Synchronous languages specify reactions of the reactive/real-time systems
to its environment within the language. This makes it easier to validate
and verify the systems relative to the assumptions and notions of
simultaneity. However, concrete embedding of the code makes it necessary to
predict time for reactions of the underlying run-time systems and
the sensors so that the strict notion of simultaneity can be relaxed
keeping the logical correctness intact. Further, for hard real-time systems,
there is a need for referring to clock times. In this paper, we describe a
method that uses timed annotations for Esterel programs that makes it
possible to predict the timing constraints on run-time system, the
sensors and clock times and validate the concrete realization relative to
time-annotated Esterel specifications. Using such time annotations, it is
possible to establish that the concrete implementation is indeed a correct
realization of the abstract system specified in annotated Esterel.
Further, the method establishes time constraints to be satisfied by the
concrete architectures for realizing the logical specification of the system.
We shall sketch the design and implementation of the tool using some of the
existing code generation tools of the Esterel environment. Furthermore, the
method can also be used for arriving at scheduling constraints on the
underlying asynchronous tasks.
