[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[David MENTRÉ]

Dear Mr Jones,

Le 04/11/2019 à 14:05, Derek M Jones a écrit :
> Ok, lets look at this paper:
> http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validating-parsers.pdf
>
>
> A common way of building a parser involves feeding a grammar into a tool
> which generates some tables, which are used by a finite state
> machine to decide whether some input conforms to a language grammar (and
> the state transitions can be used to trigger useful actions like
> building an abstract syntax tree, these actions have to be manually
> added).  The finite state machine is one component of many of a parser.
>
> This paper describes some work done to try and verify the correct
> behavior of the finite state machine.  It works by differential testing.
> A finite state machine does its job (using tables generated from an
> unverified grammar by an untrusted tool), and another tool (called
> a validator; how formal methods people love pompous names) decides
> whether it thinks the behavior of the finite state machine is correct.
>
> The paper says:
> "In summary, the approach to high-confidence parsing developed in
> this paper..."
> What is claimed is high-confidence, no claims of verified or
> guaranteed correct.

:-) Have we read the same paper?

"The second contribution is a *soundness proof* for this algorithm,
mechanized using
the Coq proof assistant, guaranteeing with the highest confidence that
if the
validation of an automaton A against a grammar G succeeds, then the automa-
ton A and the interpreter that executes it form a *correct* parser for
G." (p. 2 of the paper, bold is mine)

[...]
>
>> If those companies are using formal methods, for some of them for more
>> than 20 years, it is not due to "soap powder advertising" but due to
>> real cost benefit over several projects.
>
> Large companies are involved in a wide range of activities.
> Please provide links to sources showing real cost benefit savings.

One link (bold is mine) because I don't have much time:

    B in Large-Scale Projects: The Canarsie Line CBTC Experience
    https://link.springer.com/chapter/10.1007/11955757_21

"Beyond the technological challenge of using such a complex formal
method in an industrial context, it is now clear for us that *building
software using B is not more expensive than using conventional methods*.
Better, due to our experience in using this method, we can assert that
*using B is cheaper when considering the whole development process*
(from specification to validation and sometimes certification)."

In the paper:

"In fact, the onboard vital software was carried out with a team of 4
persons
with little knowledge of METEOR and within not much more than one year. In
addition only 25% of development time was devoted to the coding, the
remainder
was devoted to the formalization of the software specification and to
the proof.
In addition, two team members had never practised a B development even
if one
among them knew the language theoretically.
For us the main feedback is that using *B to build vital software is
effective*
and does not require a pool of experts in formal methods."


>
>> To give just one example, safety critical data verification used for
>> example in CBTC projects, goes down from 1 month to 1 or 2 days
>> (compared to manual human review process), with rapid identification of
>> faulty data and strong confidence brought to the verification process.
>
> A cost benefit analysis needs to include the startup costs.
> How much did it cost to create the tooling to automate the process? 

Tools like Atelier B (to do B Method formal development) is Component Of
The Shelf (COTS). Last time I looked, Atelier B was at ~5k€/seat/year.

Best regards,
D. Mentré


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20191208/e7b8f1a9/attachment.html>