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.