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.
Motivation
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 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.
Identified challenges
Our long-term goal of a Coq-based design and verification tool chain for reconfigurable embedded systems is very ambitious. To approach that objective, we will address in CASERM the three following challenges.
A. Modeling. Modern embedded system architectures, such as those developed using the AUTOSAR standard, involve multiple views of a given system, including logical views of application components, and physical views encompassing the assembly and mapping of application components on a given hardware architecture. They combine functional specifications with quantitative resource related constraints, and component reliability requirements. But multi-view modeling is still poorly understood, and its support in system modeling or architectural description languages remains unsatisfactory. There is also an increasing need for support of dynamicity and reconfiguration, which were until recently out of the scope of research dealing with critical real-time systems design.
B. Analysis. There are several open questions arising from the dynamical aspects of real-time systems. Classically, real-time systems are modeled and analyzed using static analysis. The parameters of the system are given, typically the periods and the Worst-Case Execution Time (WCET) of the software tasks, and their Worst-Case Response Times (WCRT) are computed thanks to a static analysis of the system. Such static analyses are also relevant to deal with systems that combine hard and soft constraints. However, when the system to be studied is subject to dynamic reconfigurations, the analysis must be performed following each reconfiguration, hence online. The main challenge we will address in this respect is twofold: (i) to introduce meaningful probabilistic constraints in real-time systems and to formulate optimization problems based on those probabilistic constraints, and (ii) to develop new online scheduling algorithms based on learning techniques.
C. Certification. Not even mentioning multiview and dynamic aspects, there are very few attempts at substantiating research results for real-time systems by mechanically proving and verifying them. Until recently, existing attempts lacked a common foundation, preventing them from being put together, and the generality and expressivity to incorporate real-world issues such as OS overheads. The Prosa initiative is an attempt at addressing this need which we intend to contribute to. An additional challenge in this area lies in the fact that it does not seem realistic to certify commercial tools performing e.g. response-time analysis without sacrificing their efficiency and flexibility. An alternative is to consider result certification, which only requires a lightweight program modification to make sure that sufficient information is logged during analysis for generating a posteriori a result certificate.
Our work program is structured around four complementary tasks: one per challenge identified above and a fourth task dedicated to case studies.
