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, 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.
The objective of this small project is to prepare the implementation of a certified tool chain for component-based and contract-based embedded systems construction, by defining a basic framework allowing the design of real-time systems that are both formally certifiable and configurable. The problems tackled in this project are to:
- 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 as to allow us to reuse results obtained by standard analysis tools (for instance, SYMTA/S for schedulability analysis)
Scientific results and exploitation.
- The main outcome of CTRC is the PERSYVAL-Lab project-team CASERM which is a joint effort between the G-SCOP, LIG and Verimag laboratories, funded for three years and a half until December 31, 2019.
- A second result is the Master thesis of Lina Marsso, on “Formal proofs for an activation model of real-time systems”, where she focused on the so-called general event load model used to describe activation patterns of software tasks. Lina formalized it and proved the correctness of the functions used to switch from the time-based view to the event-based view (and conversely) in Coq. This work provides the formal background needed to compare schedulability results based on the general event load model with results based on other activation models.
- Last, we have invited through the years 2015 and 2016 a number of renowned researchers and young academics to give talks in Grenoble (see our seminar page for the full list). These seminars have triggered many interesting discussions on the core topics of CTRC and even helped get international collaborations started.
