Search

Real-time systems are computer systems that are required not only to produce the correct output values, as a reaction to the system inputs, but also to produce these values at the correct time. In my work, I focus on hard real-time systems, where failing to respect some constraints may have catastrophic consequences. The flight-control system of an airplane, or the autonomous driving system of a car, are good examples of hard real-time systems.A real-time system can be represented as a set of concurrent tasks, where each task either senses, computes, or actuates. Each task is subject to real-time constraints, such as periodicity and deadline constraints. Reacting faster than these constraints usually does not improve the quality of the system. Instead, the main focus of hard real-time systems development is to ensure that the constraints will always be met, so as to ensure the system safety.The development of hard real-time systems involves several research domains, which are traditionally studied by separate research communities. An important part of my work focuses on the connection between these domains. My contributions concern three main topics. First, I studied the programming of real-time systems with a domain-specific synchronous data-flow language called Prelude. Second, I studied high-level timing analyses, that is to say analyses that ensure that the system will respect all its real-time constraints at execution. Third, I studied low-level timing analyses, which analyse the code of a task to determine its Worst-Case Execution Time.; Un système temps réel est un système informatique pour lequel il est nécessaire non seulement de produire les bonnes valeurs de sortie, en réaction aux entrées du système, mais aussi de produire ces sorties aux bonnes dates. Mon travail se concentre sur les systèmes temps réel dur, pour lesquels le non respect des contraintes fonctionnelles ou temporelles peut avoir des conséquencescatastrophiques. Le système de contrôle de vol d'un avion, ou encore de conduite automatique d'une voiture, sont des exemples typiques de systèmes temps réel dur.Un système temps réel peut être représenté par un ensemble de tâches concurrentes, effectuant captation, calcul, ou actionnement. Chaque tâche est soumise à des contraintes temps réel, telles que descontraintes de périodicité ou d'échéance. Réagir plus vite que ces contraintes n'améliore pas la qualité du système. La particularité du développement de système temps réel est plutôt de devoir assurer que les contraintes contraintes de temps seront toujours satisfaites à l'exécution, afin d'assurer la sûreté du système.Le développement de systèmes temps réel dur implique plusieurs domaines de recherches, traditionnellement étudiés par des communautés de recherche distinctes. Une part importante de mon travail seconcentre sur les liens entre ces domaines. Les contributions présentées dans ce document portent sur trois sujets principaux. Tout d'abord, je présente mes contributions sur la programmation desystèmes temps réel à l'aide du langage flot-de-données Prelude. Ensuite, je présente mes contributions sur l'analyse temporelle haut-niveau, dont l'objectif est d'assurer que les contraintes temps réel seront respectées à l'exécution. Enfin, je présente mes contributions sur l'analyse temporelle bas-niveau, qui détermine le pire temps d'exécution d'une tâche à partir de son code.

We present an extension of the synchronous-reactive model for specifying multi-rate systems. A set of periodically executed components and their communication dependencies are expressed in a Lustre-like programming language with features for load balancing, resource limiting, and specifying end-to-end latencies. The language abstracts from execution time and phase offsets. This permits simple clock typing rules and a stream-based semantics, but requires each component to execute within an overall base period. A program is compiled to a single periodic task in two stages. First, Integer Linear Programming is used to determine phase offsets using standard encodings for dependencies and load balancing, and a novel encoding for end-to-end latency. Second, a code generation scheme is adapted to produce step functions. As a result, components are synchronous relative to their respective rates, but not necessarily simultaneous relative to the base period. This approach has been implemented in a prototype compiler and validated on an industrial application., LIPIcs, Vol. 262, 35th Euromicro Conference on Real-Time Systems (ECRTS 2023), pages 1:1-1:22

This paper introduces a class of automata and associated languages, suitable to model a computational paradigm of fuzzy systems, in which both vagueness and simultaneity are taken as first-class citizens. This requires a weighted semantics for transitions and a precise notion of a synchronous product to enforce the simultaneous occurrence of actions. The usual relationships between automata and languages are revisited in this setting, including a specific Kleene theorem. This work is financed by the FCT – Fundação para a Ciência e a Tecnologia, I.P. (Portuguese Foundation for Science and Technology) within the project IBEX, with reference PTDC/CCI-COM/4280/2021 and project UIDB/04106/2020. published

Un système temps réel est un système dont la correction dépend non seulement des valeurs qu'il produit, mais aussi du temps quand il produit ces valeurs. La fréquence à laquelle il doit produire ces valeurs est définie par l'environnement dans lequel il opère. Un exemple typique est le système de contrôle d'un avion. Afin de garantir la sécurité de l'avion, celui-ci doit être capable de réagir dans un temps approprié à des perturbations externes tel que des rafales de vent.Quand on programme un tel système, il est important que le langage de programmation permette de raisonner sur les contraintes introduites par ce contexte. Les langages synchrones sont bien adaptés pour la programmation de systèmes temps réels critiques grâce à leur sémantique formelle et leur processus de compilation bien défini.Cependant, les systèmes temps réels et les attentes y associées ont considérablement évolués depuis la conceptions de ces langages. Dans ce travail, nous allons présenter des extensions au langage Prelude pour aborder deux limitations: La programmation de systèmes multicœur prédictible et la reconfiguration du système pendant l'exécution. 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. A typical example is an aircraft controller which must be able to react to external perturbations such as a gust of wind in a timely manner to guarantee the aircraft's safety.When programming such a system, it is important that the programming language allows to reason about the constraints introduced by this context. Synchronous languages are well-adapted to the programming of critical real-time systems thanks to their clean formal semantics and to their formally defined compilation process.However, real-time systems and their requirements have considerably evolved since the inception of these languages. In this work, we will present extensions to the synchronous language Prelude to tackle two issues: Programming multicore systems predictably and handling system reconfiguration during execution.

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.

International audience; This paper tackles the problem of designing and programming a realtime system with multiple modes of execution, where each mode executes a different set of periodic tasks. The main problem to tackle is that the period of Mode Change Requests (MCR) and the period of tasks are not all the same. Thus, not all tasks perceive MCRs in the same way. When programming such a system with traditional languages without mechanisms dedicated to mode changes (e.g. C), it is difficult to ensure a system is sound and deterministic. We propose an extension to synchronous dataflow languages to support mode changes. The semantics of the resulting language is defined formally, which prevents ambiguous programs. The language is flexible enough to support different types of mode changes. The compiler of the language includes a static analysis that rejects programs whose semantics is illdefined. The extension consists in transposing Synchronous State Machines to the Prelude language. This requires to extend the semantics of Prelude, and to define a new clock calculus, based on refinement typing.

URL editeur : http://www.springer.com/computer/journal/11704; International audience; Having a formal model of neural networks can greatly help in understanding and verifying their properties, behavior, and response to external factors such as disease and medicine. In this paper, we adopt a formal model to represent neurons, some neuronal graphs, and their composition. Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes. These archetypes are supposed to be the basis of typical instances of neuronal information processing. In this paper we study six fundamental archetypes (simple series, series with multiple outputs, parallel composition, negative loop, inhibition of a behavior, and contralateral inhibition), and we consider two ways to couple two archetypes: (i) connecting the output(s) of the first archetype to the input(s) of the second archetype and (ii) nesting the first archetype within the second one. We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings. The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings, and to express properties concerning their dynamic behavior. These properties are verified thanks to the use of model checkers. The second approach relies on a theorem prover, the Coq Proof Assistant, to prove dynamic properties of neurons and archetypes

We are interested in the programming and compilation of reactive, real-time systems. More specifically, we would like to understand the fundamental principles common to generalpurpose and synchronous languages—used to model reactive control systems—and from this to derive a compilation flow suitable for both high-performance and reactive aspects of a modern control application. To this end, we first identify the key operational mechanisms of synchronous languages that SSA does not cover: synchronization of computations with an external time base, cyclic I/O, and the semantic notion of absent value which allows the natural representation of variables whose initialization does not follow simple structural rules such as control flow dominance. Then, we show how the SSA form in its MLIR implementation can be seamlessly extended tocover these mechanisms, enabling the application of all SSA-based transformations and optimizations. We illustrate this on the representation and compilation of the Lustre dataflow synchronous language. Most notably, in the analysis and compilation of Lustre embedded into MLIR, theinitialization-related static analysis and code generation aspects can be fully separated from memory allocation and causality aspects, the latter being covered by the existing dominance-based algorithms of MLIR/SSA, resulting in a high degree of conceptual and code reuse. Our work allowsthe specification of both computational and control aspects of high-performance real-time applications. It paves the way for the definition of more efficient design and implementation flows where real-time ressource allocation drives parallelization and optimization.; Nous traitons de la programmation et de la compilation de systèmes réactifs, temps-réel. En particulier, nous cherchons à comprendre les principes fondamentaux communs à la programmation généraliste et aux langages synchrones—utilisés pour modéliser les systèmes de contrôle—et de là nous dérivons une méthode de compilation adaptée aux aspects réactifs et haute performance d’une application moderne. À cette fin, nous commençons par identifier les mécanismes des langages synchrones que SSA n’implémente pas : la synchronisation des calculs avec une base de temps externe, les entrées-sorties cycliques, et la notion sémantique de valeur absente, qui permet la représentation naturelle de variables dont l’initialisation ne suit pas de simples règles structurelles. Ensuite, nous montrons de quelle manière la forme SSA, dans l’implémentation de MLIR, peut être étendue pour implémenter ces mécanismes et leur appliquer toutes les transformations et optimisations basées sur SSA. Nous illustrons ces mécanismes par la représentation et la compilation du langage synchrone, flot de données Lustre. Nous montrons que les problèmes d’analyse statique pour l’initialisation, de génération de code, peuvent être entièrement distingués des problèmes d’allocation mémoire et de causalité, ces derniers étant pris en charge par les algorithmes d’analyse de la dominance de MLIR/SSA, ce qui permet un haut niveau de réutilisation du code et des concepts. Notre travail permet la spécification d’applications temps-réel, du point de vue du contrôle comme du calcul. Il ouvre la voie à ladéfinition de processus de conception et d’implémentation plus efficaces, où la parallélisation et l’optimisation procèdent de l’allocation des ressources temps-réel.

International audience; We introduce a systematic approach for automatically creating a visual diagram, akin to a SCADE model, from a Lustre program. This not only saves tedious manual drawing effort but also allows the creation of different views for the same program. Furthermore, we present an extension of the SCCharts language with data-flow constructs that adhere to the Lustre semantics, which in turn permits a translation from Lustre to graphical SCCharts. This allows to use the SCCharts simulation and code synthesis machinery as an alternative to existing Lustre compilation techniques. Finally, we investigate how the sequentially constructive model of computation underlying SCCharts can be used to conservatively extend Lustre, thus providing a deterministic semantics to some Lustre programs that would be rejected under its original semantics. We have implemented and validated this work with the Eclipse-based open-source KIELER framework.

The design and implementation of reactive, hard real-time systems involves modeling and generating efficient code for the integration of harmonic multi-periodic tasks. Such a reactive system can be modeled as a synchronous program orchestrating computations, state machine transitions and communications. In a harmonic multi-periodic integration program, task execution rates are related through integral ratios. This paper aims at providing a scalable way to implement large systems composed of modular, synchronous reactive tasks, and to generate efficient code satisfying real-time constraints.The paper describes three incremental extensions to the Lustre language and evaluates them on production applications. First, we propose a clock calculus for 1-synchronous clocks, i.e. strictly periodic clocks with a single activation on their period; we show how the compiler can exploit this information to raise the level of abstraction when integrating tasks at the system level. Second, we allow some variables to have unknown phases, extending the clock inference to gather constraints on unknown phases, using a solver for load balancing over multi-periodic real-time schedules, before instantiating this solution to assign clocks to all reactions of the system. Third, we propose temporally underspecified operations, relevant to many discrete control scenarii, for example on variables with low temporal variability; we show how to express this in a composable way, retaining the Kahn semantics of the synchronous program outside these controlled relaxations, and exploiting slack in the computation to relax the constraints of the real-time load-balancing problem.

This paper introduces a sort of automata and associated languages, often arising in modelling natural phenomena, in which both vagueness and simultaneity are taken as first class citizens. This requires a fuzzy semantics assigned to transitions and a precise notion of a synchronous product to enforce the simultaneous occurrence of actions. The expected relationships between automata and languages are revisited in this setting; in particular it is shown that any subset of a fuzzy synchronous language with the suitable signature forms a synchronous Kleene algebra., NORTE-01-0145-FEDER-000037. POCI-01-0145-FEDER-030947. ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciˆencia e a Tecnologia, within projects POCI-01-0145-FEDER-030947 and UID/MAT/04106/2019. The second author is supported in the scope of the framework contract foreseen in the numbers 4, 5 and 6 of the article 23, of the Decree-Law 57/2016, of August 29, changed by Portuguese Law 57/2017, of July 19. This paper is also a result of the project SmartEGOV: Harnessing EGOV for Smart Governance (Foundations, Methods, Tools) NORTE-01-0145- FEDER-000037, supported by Norte Portugal Regional Operational Programme (NORTE 2020), under the PORTUGAL 2020 Partnership Agreement, through the European Regional Development Fund (EFDR). It received further support from the PT-FLAD Chair in Smart Cities & Smart Governance

International audience; We present SASA, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. SASA is implemented as a faithful representation of the atomic-state model. This model is the most commonly used in the self-stabilizing area to prove both the correct operation and complexity bounds of self-stabilizing algorithms. SASA encompasses all features necessary to debug, test, and analyze self-stabilizing algorithms. Algorithm's properties can be checked using formal test oracles. Asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators.

International audience; Hybrid systems modeling languages that mix discrete and continuous time signals and systems are widely used to develop Cyber-Physical systems where control software interacts with physical devices. Compilers play a central role, statically checking source models, generating intermediate representations for testing and verification, and producing sequential code for simulation and execution on target platforms.This paper presents a novel approach to the design and implementation of a hybrid systems language, built on synchronous language principles and their proven compilation techniques. The result is a hybrid systems modeling language in which synchronous programming constructs can be mixed with Ordinary Differential Equations (ODEs) and zero-crossing events, and a runtime that delegates their approximation to an off-the-shelf numerical solver.We propose an ideal semantics based on non standard analysis, which defines the execution of a hybrid model as an infinite sequence of infinitesimally small time steps. It is used to specify and prove correct three essential compilation steps: (1) a type system that guarantees that a continuous-time signal is never used where a discrete-time one is expected and conversely; (2) a type system that ensures the absence of combinatorial loops; (3) the generation of statically scheduled code for efficient execution.Our approach has been evaluated in two implementations: the academic language Zélus, which extends a language reminiscent of Lustre with ODEs and zero-crossing events, and the industrial prototype Scade Hybrid, a conservative extension of Scade 6.