Context
The CASERM project represents a significant effort towards a Coq-based design and verification method for reconfigurable multi-view embedded systems. The use of a proof assistant to support such a framework is motivated by the fact that the systems that we target are both extremely complex and critical.
Embedded systems are present in our everyday life. The common characteristics shared by these systems is that, on top of functionality requirements, they must satisfy additional constraints on e.g. reactivity, reliability, and resource consumption. These constraints arise from the fact that embedded systems must adapt to their physical environment and only have limited resources. Designing and verifying embedded systems requires means to handle these multiple views of a system as well as their interaction.
The need for embedded systems to reconfigure is nowadays felt in many application domains, including safety critical ones (transport, energy, health, …). For instance, a reconfiguration may be necessary in order to adapt to a failure, to cope with new requirements, or following a hardware update. Despite of recent advances, the current state of the art does not yet provide integrated formal methods and tools for the design and analysis of reconfigurable multi-view embedded systems. This is the goal of the CASERM project.
Objectives
The Verimag teams are involved particularly in two of the four objectives :
An architecture description framework. Our ambition is to develop :
- a multiview, reconfigurable architecture description language (ADL) that is able to describe all relevant aspects (such as functional, resource related, reliability, …) of embedded systems which may evolve. The ADL will be based on the location graph formalism currently developed in the SPADES team.
- techniques and tools for the analysis of architecture descriptions which allow the reuse of viewpoint-specific analysis technology.
A formal framework for real-time analysis in Coq. Our objective is to lay the foundations for computer-assisted formal verification of schedulability analysis results. Specifically, we aim at contributing to Prosa, a foundational Coq library of reusable concepts and proofs for real-time schedulability analysis. A key scientific challenge is to achieve a modular structure of proofs for response-time analysis. We intend to use this library for : (1) a better understanding of the role played by some assumptions in existing proofs ; (2) a formal comparison of different analysis techniques ; and (3) the verification of proof certificates generated by instrumenting (existing and efficient) analysis tools.
People involved
G-SCOP GSCP team :
- Jean-Philippe Gayon
LIG/INRIA SPADES team :
- Pascal Fradet
- Alain Girault
- Gregor Goessler
- Xavier Nicollin
- Sophie Quinton
- Jean-Bernard Stefani
LIG/INRIA POLARIS team : -* Bruno Gaujal -* Stephan Plassart
Verimag :
- Susanne Graf
- Jean-Francois Monin
- Xavier Nicollin
