Analyse temporelle de systèmes cyber-physiques dirigés par les modes sous contraintes temps-réels relâchées

Cyber-Physical Systems (CPSs) are distributed systems that react to environmental stimuli using sensors. These changes are measured by sensors, processed by internal tasks, and the result is sent to various actuators. CPSs comprise dozens to hundreds of processes, often executed simultaneously. CPSs are widely used in everyday life, e.g., autonomous vehicles, industry 4.0, and smart cities. Ensuring the safety of these systems is crucial, as any malfunctions can compromise the overall functioning of the system. The subject of this Ph.D. thesis is the software malfunctioning aspect of CPSs, more specifically, the real-time aspects. Formalisms such as dataflow models allow specifying CPSs using a formal representation based on graph theory. Static analysis tools adapted to these formalisms allow system designers to check the safety properties of the specified CPS. These properties, such as consistency, liveness, and functional determinism, provide reliability guarantees prior to system deployment and execution. We compare existing dataflow formalisms in the literature to formalize and compare their expressiveness. Our work uses the PolyGraph model, which is developed in CEA List. This model is well-suited to specify and analyze CPSs with real-time constraints. A CPS specified with PolyGraph that satisfies consistency, liveness, and functional determinism properties can generate code that guarantees memory boundedness and deadlock freeness. We are interested in specifying CPSs for which some processes may not have explicit real-time constraints. Nevertheless, all processes inherit explicitly specified real-time constraints through data dependencies. Formalizing these timing constraints due to data dependencies is a complex challenge but significantly improves the timing behavior analysis of a CPS. Moreover, the static analyses of a PolyGraph specification assume that all processes have zero execution time. Our work relaxes this assumption and formalizes how processes with explicit real-time constraints influence the temporal behavior of processes without explicit real-time constraints. We also propose an extension of PolyGraph, called Real-time Mode-aware Dataflow (RMDF), to specify CPSs with a set of conditional execution branches whose activation depends on data known only at runtime. We use RMDF to specify an Advanced Driver-Assistance System (ADAS) and the Ingenuity helicopter. We also present results from runtime verification of timing constraints derived beforehand.