<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">Dear Mr Jones,</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Le 04/11/2019 à 14:05, Derek M Jones a
écrit :<br>
</div>
<blockquote type="cite"
cite="mid:23f1a61f-1117-a99e-55aa-b292803ec69b@knosof.co.uk">Ok,
lets look at this paper:
<br>
<a class="moz-txt-link-freetext"
href="http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validating-parsers.pdf"
moz-do-not-send="true">http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validating-parsers.pdf</a>
<br>
<br>
A common way of building a parser involves feeding a grammar into
a tool
<br>
which generates some tables, which are used by a finite state
<br>
machine to decide whether some input conforms to a language
grammar (and
<br>
the state transitions can be used to trigger useful actions like
<br>
building an abstract syntax tree, these actions have to be
manually
<br>
added). The finite state machine is one component of many of a
parser.
<br>
<br>
This paper describes some work done to try and verify the correct
<br>
behavior of the finite state machine. It works by differential
testing.
<br>
A finite state machine does its job (using tables generated from
an
<br>
unverified grammar by an untrusted tool), and another tool (called
<br>
a validator; how formal methods people love pompous names) decides
<br>
whether it thinks the behavior of the finite state machine is
correct.
<br>
<br>
The paper says:
<br>
"In summary, the approach to high-confidence parsing developed in
<br>
this paper..."
<br>
What is claimed is high-confidence, no claims of verified or
<br>
guaranteed correct.
<br>
</blockquote>
<p>:-) Have we read the same paper?</p>
<p>"The second contribution is a <b>soundness proof</b> for this
algorithm, mechanized using<br>
the Coq proof assistant, guaranteeing with the highest confidence
that if the<br>
validation of an automaton A against a grammar G succeeds, then
the automa-<br>
ton A and the interpreter that executes it form a <b>correct</b>
parser for G." (p. 2 of the paper, bold is mine)</p>
[...]<br>
<blockquote type="cite"
cite="mid:23f1a61f-1117-a99e-55aa-b292803ec69b@knosof.co.uk">
<br>
<blockquote type="cite" style="color: #000000;">If those companies
are using formal methods, for some of them for more
<br>
than 20 years, it is not due to "soap powder advertising" but
due to
<br>
real cost benefit over several projects.
<br>
</blockquote>
<br>
Large companies are involved in a wide range of activities.
<br>
Please provide links to sources showing real cost benefit savings.
<br>
</blockquote>
<p>One link (bold is mine) because I don't have much time: <br>
</p>
<p> B in Large-Scale Projects: The Canarsie Line CBTC Experience<br>
<a class="moz-txt-link-freetext" href="https://link.springer.com/chapter/10.1007/11955757_21">https://link.springer.com/chapter/10.1007/11955757_21</a><br>
</p>
<p>"Beyond the technological challenge of using such a complex
formal method in an industrial context, it is now clear for us
that <b>building software using B is not more expensive than
using conventional methods</b>. Better, due to our experience in
using this method, we can assert that <b>using B is cheaper when
considering the whole development process</b> (from
specification to validation and sometimes certification)."</p>
<p>In the paper:</p>
<p>"In fact, the onboard vital software was carried out with a team
of 4 persons<br>
with little knowledge of METEOR and within not much more than one
year. In<br>
addition only 25% of development time was devoted to the coding,
the remainder<br>
was devoted to the formalization of the software specification and
to the proof.<br>
In addition, two team members had never practised a B development
even if one<br>
among them knew the language theoretically.<br>
For us the main feedback is that using <b>B to build vital
software is effective</b><br>
and does not require a pool of experts in formal methods."</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:23f1a61f-1117-a99e-55aa-b292803ec69b@knosof.co.uk">
<br>
<blockquote type="cite" style="color: #000000;">To give just one
example, safety critical data verification used for
<br>
example in CBTC projects, goes down from 1 month to 1 or 2 days
<br>
(compared to manual human review process), with rapid
identification of
<br>
faulty data and strong confidence brought to the verification
process.
<br>
</blockquote>
<br>
A cost benefit analysis needs to include the startup costs.
<br>
How much did it cost to create the tooling to automate the
process?
</blockquote>
<p>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. <br>
</p>
<p>Best regards,<br>
D. Mentré</p>
<p><br>
</p>
</body>
</html>