Verimag

Embedded Software Implementation

Testing tools, compilers, algorithms, operating systems, model-driven implementation methods

Compilers, algorithms, operating systems, model-driven implementation methods

The very first Lustre compiler takes a parallel program, and produces single-loop sequential code, intended to be run on a naked machine. The code reflects the static scheduling decisions taken at compile-time. The resulting code is both efficient and safe, because the sources of non-determinism are reduced to the minimum. However, some classes of embedded systems cannot be implemented efficiently with such a compilation scheme. The group now studies distributed implementations, and/or multi-thread implementations of synchronous models.

The work on these distributed or multi-threaded implementations of synchronous languages has been performed in the context of the project RISE and several academic collaborations. In particular, P. Caspi is recognized as an expert on embedded system development, in the avionics and ground transportation domains.

 Multi-threads implementations

Multi-thread implementations are needed for systems with subcomponents that should run at various speeds; this is also the case for systems that have to deal with urgent events. In these cases, it is necessary to define an implementation on top of an operating system kernel. The approach of the group is to select carefully the functions of an OS kernel that are compulsory (threads, priorities, scheduling algorithm), and to define implementations on which determinism can be guaranteed to some point. The idea is to be able to compare the behavior of the implementation with the semantics of the original (centralized) model (for instance a Lustre program). The various results have been put in application in a complete correct-by-construction chain from Matlab/Simulink to embedded code, based on several elements:

  • a front-end that translates Simulink into Lustre;
  • several back-ends that allow to implement the Lustre model onto several types of execution platforms.

The main results are the following:

  • A Memory-Optimal Buffering Protocol for Preservation of Synchronous Semantics under Preemptive Scheduling [SYN46]
  • A Semantic-preserving multitask implementation of synchronous programs [SYN47]
  • A semantic-Preserving and Memory Efficient Implementation of Inter-Task Communication on Static-Priority or EDF Schedulers [SYN48]

In the PhD by M. Alras, the complete chain from Simulink to code has been generalized, introducing Lustre++ as an intermediate formalism: it is an extension of Lustre allowing to specify constraints that come from the peculiarities of the execution platform (OS+HW). Experiments are conducted using the Lego Mindstorm platform.

 Quasi-synchronous implementations of synchronous programs

It might be necessary to distribute the code of a program on a parallel architecture, in particular for fault-tolerance purposes. The approach is the same, from a high level formal model to an implementation, controlling that the semantics is respected. This is an important subject because many safety-critical systems — Airbus flight control systems for instance
— are specified synchronously (SCADE, Simulink) and implemented quasi-synchronously: the activation clocks of subsystems implemented on distinct computers are slightly different from what their specification requires. In a Phd thesis sponsored by Airbus, we have studied this problems and addressed it in terms of approximation topologies: the implementation should not be too far from the specification and do not diverge from it [1].

We have continued this activity with several co-authors in search for logical protocols ensuring functional equivalence between specifications and implementations, in two directions:

  • logical protocols  [2],  [3]
  • protocols based on the temporal properties of quasi-synchronous clocks  [4].

 Abstract interpretation for code optimization

This is the subject of a PhD thesis partially funded by ST (J. Le Guen) started in 2008

 "Real-Energy" programming

"Real-Energy" programming Real-time programming exists, in the sense that there are languages, compiler optimizations, implementation methods and execution environments that are specifically designed to meet timing requirements. Real-energy programming does not exist, yet.

The group has started to work on the implementations methods that can be defined for a global managing of energy consumption between the embedded software and the various device drivers in the nodes of a sensor network. Existing work in systems like TinyOS allow for a quite ad-hoc managing of energy consumption, in the driver of each hardware element. When a global policy has to be implemented, the global state of the hardware elements has to be taken into account, but this is done in a per-case basis. In fact, some of the global optimizations problems can be formulated as a controller synthesis problem. Moreover, in other application domains like systems-on-a-chip for multimedia applications, people have developed solutions based on the notion of a power manager component. Our approach will be to adopt the idea of power managers, and to try and generate them from the specifications of energy policies, by techniques similar to controller synthesis.

The first result on this subject is published in LCTES 2011.

[1] Chiheb Kossentini and P. Caspi. Approximation, sampling and voting in hybrid computing systems. In Hybrid Systems Computation and Control, HSCC06, volume 3927 of Lecture Notes in Computer Science, 2006.

[2] A. Benveniste, B. Caillaud, L. Carloni, P. Caspi, A. Sangiovanni-Vincentelli, and S. Tripakis. Communication by sampling in time-sensitive distributed systems. In 6th Intl. Conf. on Embedded Software (EMSOFT’06). ACM, 2006.

[3] A. Benveniste, P. Caspi, M. Dinatale, C. Pinello, A. Sangiovanni-Vincentelli, and S. Tripakis. Loosely time-triggered architectures based on communication by sampling. In 7th Intl. Conf. on Embedded Software (EMSOFT’06). ACM, 2007.

[4] P. Caspi and A. Benveniste. Time-robust discrete control over networked loosely time-triggered architectures. In IEEE Decision and Control Conference, Cancun, December, 2008.


Contact | Site Map | Site created with SPIP 2.1.26 + AHUNTSIC [CC License]

Logged in visitors: 6 ; visits: 461012