You are here

Verified Compilation and Worst-Case Execution Time

Safety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant, which is capable of mechanically checking the correctness of the proofs.

In this thesis, we apply formal methods to obtain safe Worst-Case Execution Time (WCET) estimations for C programs. The WCET is an important property for the development of safety-critical systems, but it requires sophisticated analyses. To guarantee the absence of errors during WCET estimation, we have formally verified a WCET estimation technique based on the combination of two main methods: a loop bound estimation and the WCET estimation via the Implicit Path Enumeration Technique (IPET). The loop bound estimation itself is decomposed in three parts: program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage, each part having been formally verified. The development has been integrated into the CompCert formally verified C compiler.

The contributions of this thesis include the formalization of techniques used to  estimate the WCET, the estimation tool itself (obtained from the formalization), and an experimental evaluation, including a comparison with state-of-the-art tools.

André Oliveira Maroneze - Celtique team
Salle Michel Métivier - Campus de Beaulieu, bâtiment 12 C - Rennes
Defense Type: 
Composition of jury: 
  • Björn Lisper, Rapporteur, Professor à l'Université de Mälardalen
  • Andrew Tolmach, Rapporteur,  Professor à Portland State University
  • Xavier Leroy, Examinateur, Directeur de recherche à Inria Rocquencourt
  • Marc Pantel, Examinateur, Maître de conférences à l'ENSEEIHT
  • Christine Rochange, Examinatrice, Professeur des universités à l'Université de Toulouse III
  • Sandrine Blazy, Directrice de thèse, Professeur des universités à l'Université de Rennes 1
  • David Pichardie, Encadrant de thèse, Professeur des universités à l'ENS Rennes
  • Isabelle Puaut, Co-Directrice de thèse, Professeur des universités à l'Université de Rennes 1