Context
The ever-increasing reliance of modern societies on embedded systems raises the twin challenges of mastering their complexity and ensuring their dependability. In particular, also in the domain of critical real-time systems, in there is an urgent need for (dynamically) reconfigurable component-based systems in order to be able to adapt a system to new conditions of the environment or to new needs.
Nevertheless, despite numerous advances of the formal methods community in that domain, it is still a challenge to guarantee the correctness of complex embedded systems which have to obey simultaneously multiple types of constraints, such as functionality, safety, security, resource usage, reconfigurability.
Objectives
The objective of this small project is to prepare the implementation of a Certified tool Chain for Component-based and Contractbased embedded systems Construction by defining the a basic framework allowing the design of real-time systems that are both formally certifiable and configurable.
The tasks carried out by the project are :
- Define an appropriate architecture description language supporting component and contract based design
- Define a language for expressing multi-viewpoint contracts and come up with a multi-viewpoint contract theory
- Formalise the defined languages and theories in Coq in view of analysing properties, in particular concerning real-time and schedulability aspects ...
- ... so us to allow us reusing results obtained by standard analysis tools (for example, SYMTA/S for schedulability analysis)
The project has been successfully terminated and continues in the Persyval project CASERM.
People involved
Verimag :
- Susanne Graf
- Jean-Francois Monin
- Xavier Nicollin
SPADES :
- Pascal Fradet
- Alain Girault
- Gregor Goessler
- Xavier Nicollin
- Sophie Quinton
- Jean-Bernard Stefani
