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

TL;DR

This paper introduces a comprehensive approach for designing and generating code for multi-periodic critical embedded systems, ensuring real-time constraints and correctness through formal proofs.

Contribution

It extends synchronous programming with high-level real-time primitives to support modular multi-periodic system assembly and provides a formally verified code generation process.

Findings

Generated code respects real-time constraints and functional semantics.

Formal proof of correctness for the compilation process.

Supports modular, hierarchical design of multi-periodic systems.

Abstract

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).