POP ART Research team

Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time

Team presentation

We focus on the problem of the safe design of real-time embedded systems. Typical application domains are safety-critical systems, such as transportation (avionics, railways, automotive), medical, manufacturing, or energy production systems. The main constraints associated with embedded systems are the bounded execution time, the bounded memory footprint, the limited bandwidth, the fault-tolerance, the ultra-high reliability, and the limited available electric power.

Designing and implementing correct safety critical embedded systems requires both formal design methods and formal models, as well as their implementation in computer assisted design tools, targeted to specialists of the application domains. We contribute to this field by proposing solutions all along the design flow, from the specification to the implementation. We develop techniques for the specification and automated generation of safe real-time embedded code for safety critical embedded systems, guaranteeing correct by construction properties (such as bounded execution time, absence of deadlocks, fault-tolerance, ...). We also develop static analysis techniques to check additional properties on the generated systems. Our specific research axes are:

Research themes

  • Component-Based Design. Component-based construction techniques are crucial to overcome the complexity of embedded systems. However, two major obstacles need to be addressed: the heterogeneous nature of the models, and the lack of results to guarantee correction of the composed system. The heterogeneity comes from the need to integrate components using different models of computation, communication, and execution, on different levels of abstraction and different time scales. The BIP component framework has been designed, in cooperation with VERIMAG, to support this heterogeneous nature. Our work focuses on the underlying analysis and construction algorithms, in particular compositional techniques and approaches ensuring correctness by construction (adapter synthesis, strategy mapping). Finally, we work on contract-based design, to reason formally about what a component assumes from its context and what it guarantees on its own behavior: we propose two flavors of contracts, with may-must modalities and with probabilities.

  • Programming for embedded systems. We tackle this problem with a strong focus on language approaches. Our first contribution concerns synchronous programming languages; in particular, we work on the modular distribution of Lucid Synchrone, on dynamic extension of the globally asynchronous locally synchronous language SystemJ, and on the time-predictive implementation of PRET-C, a synchronous extension of C. Our second contribution concerns aspect-oriented programming to specify non-functional properties separately from the base program; in particular, we work on the formalization of aspect categories. Our third contribution concerns static analysis methods to ensure safety properties of programs at compile time; in particular, we work on type systems and on abstract interpretation to verify logico-numerical properties.

  • Dependable embedded systems. Dependability is a crucial property that safety critical embedded systems must verify. We address two issues related to dependability: fault-tolerance and reliability. We design multi-criteria scheduling heuristics for multiprocessor architectures, with the aim of optimizing the execution time (period and/or latency), the reliability, and the consumed electric power. We also work on automatic program transformations (and, later, aspect weaving) to transform a fault-intolerant distributed system into a semantically equivalent fault-tolerant one, based on heartbeating and checkpointing/rollback techniques. Finally, we propose a general formal method framework, based on discrete controller synthesis (à la Ramadge et Wonham), for automating the addition of fault-tolerance.

International and industrial relations

  • European FP7 Network of Excellence ARTIST-DESIGN on Embedded Systems.
  • European FP7 STREP Project COMBEST on COMponent-Based Embedded Systems design Techniques.
  • European Artemisia Project CESAR on Cost-efficient methods and processes for safety relevant embedded systems.
  • French ANR Project VEDECY on Verification and Design of Cyber-Physical Systems.
  • French ANR Project ASOPT on Static Analysis and Optimization.
  • French ANR Project AUTOCHEM on Efficient Programming for the Chemical Machine.
  • Minalogic Pole of Competitivity Project OpenTLM on Transaction Level Modeling of Systems-on-Chips.
  • INRIA Large Scale Action SYNCHRONICS on Language Platform for Embedded System Design.
  • INRIA Associated Team AFMES on Advanced Formal Methods for Embedded Systems, with the University of Auckland (New Zeland).
  • Industrial contracts with ST Microelectronics and Dassault Systèmes.

Keywords: Control systems Real-time Safety-critical software Formal methods Synchronous languages Distribution Fault tolerance Discrete controller synthesis Component-based design Contracts

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social