We have structured our work program in CASERM around four objectives: one per challenge identified and a fourth task dedicated to case studies.
WP-A. An architecture description framework. Our first 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.
Preliminary results of WP-A are presented here.
WP-B. Online optimization methods for dynamic reconfiguration systems. Our goal here is to design online optimization algorithms for the scheduling of real-time systems, making use of learning techniques so as to achieve so-called “no regret” solutions. This means that the a priori negative impact of the scheduling choices made upon each reconfiguration of the system, made at a point in time where almost nothing is known regarding the new configuration of the system, will be compensated over the life-time of the system by the positive impact of the scheduling choices made after the online learning phase.
Preliminary results of WP-B are presented here.
WP-C. A formal framework for real-time systems analysis in Coq. Our third 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 systems 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.
Preliminary results of WP-C are presented here.
WP-D. Case studies and applications. Results of the three work packages described above are meant together to contribute to our long-term goal of a Coq-based design and verification tool chain for reconfigurable embedded systems. This means in particular that they must all apply to the same systems. Interaction and cross-fertilization between work packages will thus be ensured by common case studies.
