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 :
Theses
Complete list of metadatas

Cited literature [116 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-01155693
Contributor : Abes Star <>
Submitted on : Wednesday, May 27, 2015 - 11:28:06 AM
Last modification on : Monday, November 12, 2018 - 11:00:02 AM
Long-term archiving on : Tuesday, September 15, 2015 - 6:32:07 AM

File

2015ENMP0007.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01155693, version 1

Citation

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⟩

Share

Metrics

Record views

857

Files downloads

662