Research

Overall Objectives

The Spades project-team aims at contributing to meet the challenge of designing and programming dependable embedded systems in an increasingly distributed and dynamic context. Specifically, by exploiting formal methods and techniques, Spades aims to answer three key questions:

  1. How to program open networked embedded systems as dynamic adaptive modular structures?

  2. How to program reactive systems with real-time and resource constraints on multicore architectures?

  3. How to program reliable, fault-tolerant embedded systems with different levels of criticality?

These questions above are not new, but answering them in the context of modern embedded systems, which are increasingly distributed, open and dynamic in nature , makes them more pressing and more difficult to address: the targeted system properties – dynamic modularity, time-predictability, energy efficiency, and fault-tolerance – are largely antagonistic (e.g., having a highly dynamic software structure is at variance with ensuring that resource and behavioral constraints are met). Tackling these questions together is crucial to address this antagonism, and constitutes a key point of the Spades research program.

A few remarks are in order:

  • We consider these questions to be central in the construction of future embedded systems, dealing as they are with, roughly, software architecture and the provision of real-time and fault-tolerance guarantees. Building a safety-critical embedded system cannot avoid dealing with these three concerns.

  • The three questions above are highly connected. For instance, composability along time, resource consumption and reliability dimensions are key to the success of a component-based approach to embedded systems construction.

  • For us, “Programming” means any constructive process to build a running system. It can encompass traditional programming as well as high-level design or “model-based engineering” activities, provided that the latter are supported by effective compiling tools to produce a running system.

  • We aim to provide semantically sound programming tools for embedded systems. This translates into an emphasis on formal methods and tools for the development of provably dependable systems.

Last activity report : 2013

Collaborative Projects

  • ANR PiCoq project
  • ANR Rever project
  • Team association with the Department of Electrical and Computer Engineering of the University of Auckland (New Zealand)
  • Contract with ST Microelectronics for the PhD of Vagelis Bebelis and Quentin Sabah.