Temporal Refinement for Lustre

International audienceThis paper proposes a refinement calculus for Lustre. First a very general calculus is provided, which ensures correctness and reactivity for a large class of systems. Then, this calculus is adapted to provide oversampling and temporal refinement. We obtain thus an effective calculus for Lustre, which allows us to refine both computations and time. We illustrate its use on a small example and conclude by proposing some future research perspectives