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

Official Media Partners

Supported by