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:
How to program open networked embedded systems as dynamic adaptive modular structures?
How to program reactive systems with real-time and resource constraints on multicore architectures?
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 : 2016
- Associate team Causalysis with University of Pennsylvania, Philadelphia (USA).
- ANR-PRCI project RT-PROOFS with MPI-SWS, TU Braunschweig, Verimag and Onera.
- Persyval-Lab Project Team CASERM with Verimag and LIG.
- Contract with Thales for the PhD thesis of Christophe Prévot.
- Contract with Orange for the PhD thesis of Arash Shafiei.
Past collaborative projects
- Persyval-Lab Exploratory Project CTRC with Verimag
- Associate team RIPPES with the EECS Department at UC Berkeley (USA) and the Department of Electrical and Computer Engineering of the University of Auckland (New Zealand)
- ANR PiCoq project
- ANR Rever project
- Contract with ST Microelectronics for the PhD theses of Vagelis Bebelis and Quentin Sabah