Programmation de systèmes temps réels adaptatifs

A real-time system is a system whose correctness depends not only on the correctness of the values it produces, but also on the time when it produces those values. The rate at which it must produce values is defined by the environment it operates in. When programming such a system, it is important that the programming language allows to reason about the constraints introduced by this context. Synchronous languages [14] are well-adapted to theprogramming of critical real-time systems thanks to their clean formal semantics and to their formally defined compilation process. In this work, we will present extensions to the synchronous language Prelude [67] to tackle two issues: Programming multicore systems predictably and handling system reconfiguration during execution.Multicore hardware platforms have the potential to increase the performance of real-time systems. However, their architecture, especially the shared central memory, is prone to hard-to-predict delays, outweighing the potential benefits. To address this issue, models such as PREM [71] and AER [32] have been proposed. Our first contribution aims at producing AER-compliant multicore C code from a high-level Prelude program. This shifts the responsibility of low-level implementation concerns related to task communications onto the compiler, saving tedious and error-prone development efforts.A multi-mode real-time system must respect different functional requirements during its execution. A mode of execution represents a possible system configurations, for an aircraft control system these may include take-off, cruise and landing. Mode change protocols define transitions to change safelyfrom one mode to another. Our second contribution proposes clock views to decouple the rate of tasks and transitions. The resulting multi-mode support is both formally defined and generic enough to allows programmers to choose the kind of protocol they need for their application. A clock calculus based on refinement typing [39, 83] infers and checks the consistency of rates and views.Un système temps réel est un système dont la correction dépend non seulement de la correction des valeurs qu’il produit, mais aussi du temps quand il les produit. Le rythme de production de ces valeurs est défini par l’environnement dans lequel il opère. La programmation d’un tel système nécessite un langage de programmation permettant de résonner sur les contraintes introduites par ce contexte. Les langages synchrones [14] sont bien adaptés pourla programmation de systèmes critiques temps réel de part leur sémantique et leur processus de compilation formellement définis. Dans ce travail, nous présentons des extensions au langage synchrone Prelude [67] pour aborder deux problèmes : La programmation de systèmes multicœur prédictibleset la reconfiguration du système durant l’exécution.Les plateformes matérielles multicœurs possèdent un potentiel de performances accrues des systèmes temps réel. Cependant, leur architecture, en particulier la mémoire centrale partagée, est sujette à des délais difficiles à prédire, contrebalançant les gains potentiels. Les modèles tel que PREM [71] et AER [32] remédient à cette limitation. Notre première contribution permet de produire du code multicœur en accord avec le modèle AER à partir d’un programme haut-niveau Prelude. Ceci permet de transférer la responsabilité des problèmes bas niveau liés aux communications inter-tâches, évitantdes efforts de développement fastidieux et sujets aux erreurs. Les exigences fonctionnelles d’un système temps-réel multi-mode évoluent durant son exécution. Un mode d’exécution représente une configuration possible du système, par exemple décollage, croisière ou atterrissage pour un système de contrôle d’avion. Les protocoles de changement de mode définissent des transitions afin de changer de mode en sécurité. Notre seconde contribution propose les vues d’horloge pour découpler le rythme d’exécution des tâches de celui des transitions. Le mécanisme multi-mode résultant est à la fois formellement défini et générique afin de permettre de choisir le type de protocole approprié à application. Un calcul d’horloge basé sur le typage par raffinement [39, 83] infère et vérifie la cohérence des rythmes et vues