The synchronous Logical Execution Time paradigm

International audienceReal-Time industrial systems are not so much of those that have to perform tasks incredibly fast, but in a timepredictable manner; they rather focus on meeting previously specified timing requirements in a provable way. Consequently, time must be taken into account from the very start of the design. However, exact timing constants may not be available yet inearly design stages as they may depend on the target. In answer, formalisms based on the Multiform Logical Time have been introduced to abstract real-time durations. The Synchronous-Reactive (SR) approach introduced a discretized abstraction of time on which computations happen logically instantaneously. Contrary to SR, Logical Execution Time (LET) mandates to specify the actual logical duration a task has to fulfill. This allows a more efficient compilation, at the price of a lower expressiveness. Classical LET (i.e. as introduced in Giotto/TDL) sticks to uniform pseudo-physical time, i.e. based on one logical clock mapped to the real-time. In this paper, we introduce a new paradigm called synchronous Logical Execution Time (sLET) that builds upon both SR and LET paradigms. It keeps the idea of logical durations coming from the LET paradigm, while having logical instants based on logical clocks. This extends the expressivity of LET, as time is totally abstracted as sequences of events. The various schedulings provide physically timedversions that, while having distinct non-functional properties (in terms of performance mostly), remain mutually functionally equivalent (in the logical time realm). A particular instance, where computations are executed ”in a single instant”, and then time is advanced (as in classical event-driven simulation), can lead to a direct translation into synchronous formalisms (in our case Esterel). We started inquiring how this could open new ways of verification and analysis on PsyC program