Execution supports

The Real-Time System team is developing Trampoline, a real-time operating system compatible with OSEK/VDX and AUTOSAR 4 distributed under free license. The development of Trampoline started in 2005 and was supported by two FUI: O4A Pilot and O4AII. The development of Trampoline was undertaken to meet two objectives :

have an operating system that is both free and compatible with an industry standard. As such, Trampoline is used for teaching and is used industrially by See4sys Technologie and is part of Dassault Systems' AUTOSAR core software offering.

have a support allowing the prototyping of research work.

Trampoline is operated in two ANRs: Respected and ImpRo.

TRAMPOLINE : http://trampoline.rts-software.org

Transactional memories appear today as a promising solution to manage concurrent access to shared variables on multicore execution platforms. Contrary to locking-based approaches (e.g. semaphores, spinlocks, etc.) which can reintroduce execution sequentiality in the application due to the blocking times on locks, transactional memory-based mechanisms allow to exploit to the maximum the parallel execution capabilities of multicore platforms.

In this context, we are interested in:

the design and analysis of non-blocking transactional memory-based protocols adapted to hard real-time systems (wait-free progress guarantees);
STM-HRT: http://stmhrt.rts-software.org

the proposal of a formal verification methodology of the functional validity of these protocols using model-checking approaches.

Scheduling

The massive adoption of multiprocessor/multicore hardware architectures for the execution platforms of embedded real-time systems has led us, for several years, to consider multiprocessor real-time scheduling. After having carried out various evaluation and comparison studies of its numerous scheduling policies using a simulation approach, our
research turned to the problem of their implementation within a real-time operating system, namely Trampoline (the real-time operating system developed by our team). In addition to the study of the feasibility of implementing new multiprocessor scheduling policies in Trampoline, the objective is also to accompany it with a formal verification work to ensure the functional and temporal correctness of the implemented schedulers.

To start with, the implementation of the G-EDF and EDF-US global scheduling policies was performed, the first one being based on fixed priorities for jobs while the second one mixes fixed priorities for tasks and fixed priorities for jobs. For each of them, the formal modeling built from the Trampoline source code using timed automata has been extended to scheduling-related components. A set of behavioral requirements to be met by each of them
was specified and led to the development of observer models. Finally, accessibility tests of some of their states allow deciding on the respect of the requirements and more generally, the correction of the considered scheduling policy.

This approach, which is intended to be as generic and safe as possible, now needs to be tested more widely, particularly with respect to the implementation of more elaborate scheduling policies, especially those that aim at optimality.

In intelligent wireless sensors, timing constraints are increasingly combined with energy constraints. Human intervention is also limited or prohibited because these systems are either inaccessible or deployed in too large numbers or in hostile environments. They operate with batteries and/or super-capacitors that are continuously recharged by a renewable energy source, e.g. solar energy, piezoelectric energy, etc. Designing such fully autonomous embedded systems requires the resolution of multidisciplinary problems related to the harvesting of ambient energy, its storage and use, so as to ensure an autonomy of one to ten years, while maintaining an acceptable level of performance of the real-time processing system.

The problem addressed concerns the proposal and validation of real-time scheduling mechanisms, in charge of adapting the activity of the processor(s) to the profile of the ambient energy source in order to guarantee what is known as "energy neutrality".

For hard real time applications, it is necessary to determine the minimum size of the energy reservoir that will guarantee both energy neutrality and compliance with the timing constraints expressed in terms of deadlines. This also implies designing scheduling and dynamic power management mechanisms that dynamically take into account the energy consumed as well as the energy produced.

For applications with firm constraints, the scheduling of tasks must make it possible to optimise a Quality of Service criterion, in this case the ratio of satisfied deadlines, when the available energy is insufficient to satisfy all the timing constraints over the entire life of the application.

Formal methods

The members of the formal methods theme are interested in rigorous (mathematical) system modeling, automatic or semi-automatic verification of their correction, and the synthesis of correct-by-construction systems.

In particular, for systems in which time must be explicitly taken into account, formalisms such as time Petri nets or time automata are used.

Recent topics studied include distributed timed systems and exploitation of concurrency, as well as parametric timed systems. These allow a system to be modelled by leaving certain timing features (transmission delay, activation period, etc.) unspecified and it is the verification process that will determine all the possible values to satisfy the desired properties.

A tool, called Roméo, is the main target for the implementation of the techniques developed within the theme of formal methods.

Romeo allows in particular the modeling of systems through a language similar to time Petri nets, the use of time parameters, the modeling of preemptions, and the verification of properties expressed in a timed and parametric temporal logics.

Roméo is used in pedagogy for several master 2 level courses but also in the context of industrial collaborations (Sodius, Dassault Aviation, Thales Research, Huawei).

Networks and protocols of the Internet of Things (IoT)

The Internet of Things (IoT) brings together a substantial set of wireless network protocols with variable ranges from personal area (WPAN) to low power wide area network (LPWAN) making it possible to address a large number of use cases. In the team, we are interested in this technological set by questioning the notions of interoperability, energy consumption, Internet protocol compatibility (in particular through the SCHC initiative at the IETF), security and algorithms-hardware architectures matching. Current use cases concern sensor networks within a micro-data center to optimize the cooling system and valorise the heat produced or to help sub-Saharan populations to adapt to climate change. For us, the Internet of Things also concerns underwater objects (Internet of Underwater Things, IoUT) with applications in ocean engineering or maritime ecosystem monitoring. This research topic involves designing level 2 and level 3 (and beyond) protocols adapted to acoustic communications widely used in the underwater context. The adaptation of existing embedded systems is also within the prerogatives of the topic to verify in situ the proposed mechanisms during experimental campaigns at sea. The theme is counting numerous academic, industrial, national or international collaborations.

contact : Benoît Parrein, Ass. Professor Nantes Université : benoit.parrein@ls2n.fr