Implementing Multi-Periodic Critical Systems: from Design to Code Generation

Julien Forget (1) , Frédéric Boniol (1, 2) , David Lesens (3) , Claire Pagetti (1, 2)

1 ONERA - The French Aerospace Lab [Toulouse]
2 ENSEEIHT - Ecole Nationale Supérieure d'Electrotechnique, d'Electronique, d'Informatique, d'Hydraulique et de Télécommunications
3 AST - Astrium Space Transportation

This article presents a complete scheme for the development of Critical Embedded Systems with Multiple Real-Time Constraints. The system is programmed with a language that extends the synchronous approach with high-level real-time primitives. It enables to assemble in a modular and hierarchical manner several locally mono-periodic synchronous systems into a globally multi-periodic synchronous system. It also allows to specify flow latency constraints. A program is translated into a set of real-time tasks. The generated code (C code) can be executed on a simple real-time platform with a dynamic-priority scheduler (EDF). The compilation process (each algorithm of the process, not the compiler itself) is formally proved correct, meaning that the generated code respects the real-time semantics of the original program (respect of periods, deadlines, release dates and precedences) as well as its functional semantics (respect of variable consumption).

Domaines: Systèmes embarqués

Julien Forget, Frédéric Boniol, David Lesens, Claire Pagetti. Implementing Multi-Periodic Critical Systems: from Design to Code Generation. FM-09 Workshop on Formal Methods for Aerospace, Nov 2009, Eindhoven, Netherlands. pp.34-48. ⟨hal-00800990⟩