Skip to Main content Skip to Navigation

Static analysis of control-command systems : floating-point and integer invariants

Abstract : A critical software is a software whose malfunction may result in death or serious injury to people, loss or severe damage to equipment or environmental harm.Software engineering for critical systems is particularly difficult, and combines different methods to ensure the quality of produced software.Among them, formal methods can be used to prove that a software obeys its specifications.This thesis falls within the context of the validation of safety properties for critical software, and more specifically, of numerical properties for embedded software in control-command systems.The first part of this thesis deals with Lyapunov stability proofs.These proofs rely on computations with real numbers, and do not accurately describe the behavior of a program run on a platform with machine arithmetic.We introduce a generic, theoretical framework to adapt the arguments of Lyapunov stability proofs to machine arithmetic.A tool automatically translates the proof on real numbers to a proof with floating-point numbers.The second part of the thesis focuses on linear relation analysis, using an abstract interpretation based on the approximation by convex polyhedrons of valuations associated with each control point in a program.We present ALICe, a framework to compare different invariant generation techniques.It comes with a collection of test cases taken from the program analysis literature, and interfaces with three tools, that rely on different algorithms to compute invariants: Aspic, iscc and PIPS.To refine PIPS results, two code restructuring techniques are introduced, and several improvements are made to the invariant generation algorithms and evaluated using ALICe.
Document type :
Complete list of metadata

Cited literature [116 references]  Display  Hide  Download
Contributor : ABES STAR :  Contact
Submitted on : Wednesday, May 27, 2015 - 11:28:06 AM
Last modification on : Wednesday, November 17, 2021 - 12:31:47 PM
Long-term archiving on: : Tuesday, September 15, 2015 - 6:32:07 AM


Version validated by the jury (STAR)


  • HAL Id : tel-01155693, version 1


Vivien Maisonneuve. Static analysis of control-command systems : floating-point and integer invariants. Other [cs.OH]. Ecole Nationale Supérieure des Mines de Paris, 2015. English. ⟨NNT : 2015ENMP0007⟩. ⟨tel-01155693⟩



Record views


Files downloads