Cost effective robustness verification of control software with Frama-C: lessons learnt and perspectives
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.