Implementation of Real-Time Systems on Many-Core Architectures
The group is working on languages and tools for the implementation of critical real-time reactive systems. One success story in this area is the Lustre language.
We are working on extensions of the language to allow exploiting the parallelism of many-core architectures (both symmetric multiprocessing and network-on-chip based architectures). We are particularly interested in Kalray’s MPPA processor. We base our current work on multi-thread implementation of synchronous languages, where we defined a communication protocol allowing deterministic communications even in the presence of timing variations. We started a CIFRE Ph.D with Kalray on the subject in 2015.
Worst-Case Execution Time Analysis
Synchronous languages like Lustre allow reasoning and proving properties on the program regardless of its temporal behavior. However, the implementation has to satisfy some timing constraints. A complete implementation flow must therefore include not only tools to show the functional correctness and code generators, but also tools to analyze the Worst-Case Execution Time (WCET) of the generated code and show that its execution will meet the deadlines.
Our approaches combines low-level information (about the final executable) and high-level ones (from the source code in C or in Lustre). The high-level information allow cutting some unfeasible path in the analysis and improves the WCET estimation compared to a purely low-level analysis. The path-aware analysis can be done in multiple ways, either adding constraints in the final step of the traditional ILP-based analysis, or with a new approach based on Satisfiability Modulo Theory (SMT).
We are also interested in architecture modeling to compute a WCET bound for programs running on multi- or many-core architectures, in particular Kalray’s MPPA processor which we study in the CAPACITES project.
Mixed Criticality Systems
We are interested in performance related analyses for mixed critical and weakly hard systems — which allow certain safety properties to be violated under the condition that this doe not happen too often. For example, for Response Time Analysis, we may rely on Typical Case instead of Worst Case Execution Time.
Different aspects (timing, functionality, dependability, ...) are analysed independently in critical systems. In weakly hard systems, the strong hypotheses guaranteeing the independence of different aspects must be replaced by explicit assumptions. The challenge is to allow the users to continue using their usual tools by linking assumtions in aspect 1 to guarantees in aspect 2, despite the fact that they express constraints on different event sets, and more generally rely on different theories.