Cost effective robustness verification of control software with Frama-C: lessons learnt and perspectives

Emmanuel Ledinot

Head of Scientific Studies, R&T and Business Development Directorate, Dassault Aviation

Robustness testing is a difficult task. In this talk we report on a successful attempt to circumvent part of robustness testing by means of static analysis. Absence of run-time errors and functional robustness properties (out of range variables, precondition violation) are proved on SCADE models by means of abstract interpretation and theorem proving jointly working through the Frama-C kernel.

When facing numerical assertions that are too complex to be proven within the alloted verification budget, massive local random testing is used on sound statically-computed ranges. As a consequence, the validity statuses of these assertions become probability confidence intervals instead of booleans.

The benefits and limits of cooperative static-dynamic verification will be disccussed, as well as prospective views on contract-based development and mutiparadigm integration verification.

About Emmanuel Ledinot

Emmanual LeDinot is a senior expert in formal methods applied to software and system engineering at Dassault-Aviation and was Dassault’s representative in the ED-12/DO-178 formal methods group. Ledinot graduated as an engineer from Centrale Paris and has an MS in theoretical computer science from the University of Paris VII.

Sponsored by

Supported by