[SystemSafety] Empirical Study on the Correctness of, Formally Verified Distributed Systems

José Miguel Faria jmf at safeperspective.com
Fri Apr 21 17:31:00 CEST 2017


Derek,

Yes, I let the snake oil salesmen in formal methods drag me
> down to their level.

:) :)

Given X resources, which technique produces the most
> reliable software?  Alternative, which technique can most cheaply
> deliver reliability Y?


That is certainly an open question. And I can't think of a "perfect" way of
quantifying data to come up with such an answer.
Actually, I don't believe in a definitive single answer. Different problems
are better solved with different approaches. The strategy I like the best
is to be conversant enough in a multitude of techniques so that you can
"feel" which one will best tackle a given problem.

For example, I've personally used "formal methods" (TLA+) in this
<http://www.springer.com/us/book/9781441997357> industrial project and I
can't think of a technique that would have produced better results for that
context.
On the other hand, for many other contexts, there are certainly far better
approaches.

What does using "formal methods" actually mean?
> http://shape-of-code.coding-guidelines.com/2016/08/29/does-
> using-formal-methods-mean-anything/

Certainly agree with your "soap power" remarks. It doesn't make it better,
but maybe there is some field in academia where people don't pick a fine
selection of words to exacerbate the results they achieve in a paper? :)

This paper provides an engineering view of using maths to
> show properties:
> https://alastairreid.github.io/papers/fmcad2016-trustworthy.pdf

Will give it a read, thanks.


José

On Fri, Apr 21, 2017 at 3:38 PM, Derek M Jones <derek at knosof.co.uk> wrote:

> José,
>
> As it reads, the quoted text might be a bit misleading. For the sake of
>> completeness, I'd add a bit more of text extracted from the paper:
>>
>
> Yes, I let the snake oil salesmen in formal methods drag me
> down to their level.
>
> On the positive side, still from the paper: "The absence of protocol bugs
>> found in the verified systems sharply contrasts with the results of an
>> analysis we conducted of known bugs in unverified distributed systems."
>>
>
> The comparison needs to be against systems verified using other
> techniques.  Given X resources, which technique produces the most
> reliable software?  Alternative, which technique can most cheaply
> deliver reliability Y?
>
> What does using "formal methods" actually mean?
> http://shape-of-code.coding-guidelines.com/2016/08/29/does-
> using-formal-methods-mean-anything/
>
> This paper provides an engineering view of using maths to
> show properties:
> https://alastairreid.github.io/papers/fmcad2016-trustworthy.pdf
>
>
> --
> Derek M. Jones           Software analysis
> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20170421/f9b4bd31/attachment.html>


More information about the systemsafety mailing list