PhD Thesis and Formal Developments

This page contains a link to the manuscript of my PhD thesis (updated on 2014-06-24) and a summary of the online formal developments described in the thesis.

The subject of my PhD thesis is: Verified Compilation and Worst-Case Execution Time Estimation. The abstract below describes it in more detail.

Abstract

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 – built upon solid mathematical bases – 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 – a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence.

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 related to the safety of critical systems, but its estimation requires sophisticated techniques. 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 steps: a program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage. Each stage has a chapter dedicated to its formal verification. The entire development has been integrated into the formally verified C compiler CompCert. We prove that the final estimation is correct and we evaluate its performances on a set of reference benchmarks.

The contributions of this thesis include (a) the formalization of the techniques used to estimate the WCET, (b) the estimation tool itself (obtained from the formalization), and (c) the experimental evaluation.

We conclude that our formally verified development obtains interesting results in terms of precision, but it requires special precautions to ensure the proof effort remains manageable. The parallel development of specifications and proofs is essential to this end. Future works include the formalization of hardware cost models, as well as the development of more sophisticated analyses to improve the precision of the estimated WCET.

Formal development

The formal development related to this thesis (including Coq definitions and proofs, as well as non-proved code related to the implementation) are available in this archive.

Verified Validation of Program Slicing

The formal development of a scalable program slicing validator. This program slicer is related to the one used in the loop bound analysis described below, but it contains a separate correctness theorem, as well as a more efficient and up-to-date implementation.

WCET-Oriented Loop Bound Analysis

The formal verification of a loop bound estimation, including three separate components (program slicing, value analysis and bounds estimation).

Verified Value Analysis for CompCert

The development of a formally verified value analysis for C programs, which can be used to perform other analysis and prove properties such as memory safety. This analysis is directed towards safety-critical software.

IPET-based WCET estimation (link to the PDF article)

This paper summarizes the development related to the final part of the tool, namely the IPET-based WCET estimation.



Return to the main page