Benchmarking The Scalability of Model-checker-based

Description du poste **Domaine**: - Mathématiques, information scientifique, logiciel **Contrat**: - Stage **Intitulé de l'offre**: - Benchmarking the scalability of model-checker-based detection of timing anomalies H/F **Sujet de stage**: - Safety-critical systems such as autonomous vehicles and modern avionic computers have to satisfy strong timing requirements. A failure to meet a timing constraint, missing a deadline for example, may result in serious malfunctions. Therefore, it is crucial to compute safe timing bounds for these systems. **Durée du contrat (en mois)**: - [3 à 6 mois] **Description de l'offre**: **Rejoignez-nous en Stage ** - Worst-Case Execution Time (WCET) analyses compute sound and (desirably) tight worst-case execution bounds, exploring, via convenient abstractions, all the execution paths of a program running on a computer architecture. This process is complicated by the presence of Timing Anomalies (TA) [1], a counterintuitive behavior in the sense that the local worst-case timing behavior, typically due to a cache miss, does not result in the global worst-case performance. TAs thus require an exhaustive exploration of the reachable hardware states, which is costly or often even prohibitive.The LECA laboratory has developed a framework to detect TAs [2, 3] within programs, that is based on a formal model of a representative Out-of-Order (OoO) pipeline of processors described using the TLA+ high-level language [4]. The output of the gem5 simulator is used to generate program specifications from input C source codes, and local timing variations are generated using heuristics targeting the latencies of memory instructions. Finally, TA is expressed as an hyper-property in TLA+ and formally verified with the TLC model-checker over a combined formal model of the pipeline and a program.A first goal of this internship is to evaluate the scalability of this workflow, in particular for identifying the lifetime of TAs but also their patterns. It requires to represent in the formal specification of programs the notion of basic blocks, the atomic analysis unit in static WCET analyses. This will enable to study whether TAs can propagate across several basic blocks and help to capture the limits of the workflow. These evaluations will be performed on an higher number of source codes from the TACLe benchmarks than currently supported. Another goal of this internship is then to study how the scalability of this workflow can be optimized by either using the output of WCET cache analyses to narrow the set of latency variations, vary the verification instant for the detection of TAs or by using different model-checkers, such as the Apalache symbolic model-checker for TLA+ [5].[1] T. Lundqvist et al., “Timing anomalies in dynamically scheduled microprocessors,” in Real-Time Systems Symposium, 1999.- [2] M. Asavoae et al. Formal executable models for automatic detection of timing anomalies. In: 18th International Workshop on Worst-Case Execution Time Analysis, WCET 2018. pp. 2:1-2:13 (2018).- [3] B. Binder, et al., "Is This Still Normal? Putting Definitions of Timing Anomalies to the Test," 2021 IEEE 27th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Houston, TX, USA, 2021, pp. 139-148.- [4] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)- [5] Igor Konnov et al. TLA+ model checking made symbolic. Proc. ACM Program. Lang. 3, OOPSLA, Article 123 (October 2019).**Moyens / Méthodes / Logiciels**: - Méthodes formelles, micro-architecture, temps réel - Computer engineering student (final year) or master 2 student with knowledge in computer architecture, and formal methods, in particular model checking. Communication and writing skills, teamwork motivation and eager to learn.In line with CEA's commitment to integrating people with disabilities, this job is open to all.Localisation du poste **Site**: - Saclay **Localisation du poste**: - France, Ile-de-France, Essonne (91) **Ville**: - Palaiseau **Langues**: - Anglais (Intermédiaire) **Diplôme préparé**: - Bac+5 - Diplôme École d'ingénieurs Demandeur **Disponibilité du poste**: - 01/03/2025 Informations générales **Entité de rattachement**: Le CEA est un acteur majeur de la recherche, au service des citoyens, de l'économie et de l'Etat. Il apporte des solutions concrètes à leurs besoins dans quatre domaines principaux : transition énergétique, transition numérique, technologies pour la médecine du futur, défense et sécurité sur un socle de recherche fondamentale. Le CEA s'engage depuis plus de 75 ans au service de la souveraineté scientifique, technologique et industrielle de la France et de l'Europe pour un présent et un avenir mieux maîtrisés et plus sûrs. Implanté au cœur des territoires équipés de très grandes infrastructures de recherc