Re: [SystemSafety] Scalability of Formal Methods [was: Logic]

From: David MENTRE < >
Date: Wed, 26 Feb 2014 15:13:54 +0100


Hello Peter,

Le 26/02/2014 12:30, Peter Bernard Ladkin a écrit :
> For example, David tells us that a couple hundred thousand lines of Ada source have been formally
> verified in 2006 using Atelier B. Now, if that was all SPARK source I would be prepared to believe
> it, but I'd want to know how many proof obligations were left undischarged.

Zero (0). Of course, a significant part (3.3% to 8.1% of proof obligations, i.e. 1,400 to 2,200) is done manually (i.e. interactive proofs) by a team of skilled engineers (internal or using subcontracts to companies specialized in such proofs).

B Method is based on refinement: you start from a formal specification, then you add details (algorithms, data structures) until you reach the B0 level which corresponds to a basic programming language (IF, WHILE, Boolean, integers, arrays, ...). At this level, you can directly translate it in Ada or C. At each refinement step, proof obligations are automatically generated to ensure the refined code corresponds to the more abstract one.

For the translation to Ada or C part, usually a double translator is used: two translators, developed by different teams with different technologies, one checks the result is the same[1].

> If it isn't all SPARK
> source, then I become more wary. Also, my experience tells me that, of any industrial system with
> reliability requirements, 90%-95% of the source code is boilerplate. Boilerplate is functionally
> simple and easy formally to verify; furthermore, it is repeated all over. So 95% of your functional
> code is going to be easy formally to verify, if you are organised and put in the effort. But that 5%
> - now that could really do you in! It's theorem-proving and the math might do you in, even with the
> best prover technology.

I agree. That's why, when applying formal methods:

Sincerely yours,
david

[1] Somebody like Nancy Leveson could wonder if such double translator approach is really safe. I would say that such translators are rather basic (no complex algorithm) and the specification are rather clear, so we can have good arguments to say it is safe.

[2] Even after careful review by experts, some errors might slip in. Later studies with formal methods (e.g. Coq proof assistant or Zenon automated prover) have indeed found errors (e.g. 20 over 274 examined rules). But those errors where minor (correct rule but incorrect manual proof, or issues on non-freeness of rule variables) and never leaded to a proof obligation that was wrongly proved correct.



The System Safety Mailing List
systemsafety_at_xxxxxx Received on Wed Feb 26 2014 - 15:14:06 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST