[trustable-software] The DeepSpec project...

Feuer, Magnus mfeuer1 at jaguarlandrover.com
Sun Feb 5 23:48:04 UTC 2017


[lurk-mode: off]

Oooh. Something I've actually worked with in a previous life. [1]

Disclaimer: The information below is probably out of date, but I can find
out more.

Formal verification has traditionally been done on well-contained
signal-based systems that lends themselves to Boolean algebra. Typical
examples are nuclear power plants, train signalling, aircraft systems, and
other safety-critical systems. Applying formal verification to these
systems allows you to ask questions such as "When is the landing gear
deployment signal set and the speed is greater than 250 knots?" (which
would rip the landing gears off the plane).

This is all well and good when you work with discrete signals. Things get a
*lot* more complicated when you work with generic programming languages
that has a much more complex and hard-to-determine state. The questions
that are hardest to answer (in my possibly outdated experience) is "Which
in-parameters to function foo() will return a value greater than 4711?".

Paul, you are right that there is a bit of a reality gap between the formal
verification people, who tend to be hard-core mathematicians, and the
grimy, bitter husks of human beings (such as you and me) that do automotive
software.

In my experience is that you get the best result you both adapt the formal
verification system to the development tools *and* constrain said tools to
better suit formal verification. One such example is an asynchronous,
signalling based system, which inherently is more discreet and easier to
verify than a (contract-less) API.

By chance, I am starting to read up on formal verification again for an
internal project I am working on. I will, in other words, be more up to
date on the subject in a couple of weeks, should there be interest.

A somewhat less strict testing method would be domain-based testing. I
haven't worked with that myself but have colleagues swearing by it. The
Quickcheck site describes it better than I would ever could. [2].
Please tell me if you want more info on this, and I will dig around.

[1] http://prover.com
[2] http://www.quviq.com/products/erlang-quickcheck/ (Never mind the Erlang
bit; domain-based testing is language-agnostic.)


Sincerely,

/Magnus F.


On Sun, Feb 5, 2017 at 1:55 PM, Paul Sherwood <paul.sherwood at codethink.co.uk
> wrote:

> Hi all,
> Edmund brought the DeepSpec project to my attention a couple of days ago,
> and I think it may be of interest both to the trustable community and
> Safe-Secure-C wizards.
>
> I find it particularly interesting to see research on bringing formal
> mathematical rigour to C language, tooling and interfaces.
>
> My own limited exposure to formal methods over the years has led to a
> couple of observations:
>
> - I've found it hard to have productive communication with advocates of
> formal methods: they probably conclude I'm too dumb for their concepts,
> while I conclude their concepts are likely to be too difficult for normal
> engineers
>
> - the communication gap makes me worried that formal methods folk may
> create solutions which are theoretically fantastic, but don't address
> practical realities
>
> However, as Niall said in the early discussions here [2] maybe the best we
> can do is to aim for trustability only for minority of core software, as a
> safe sandpit for the majority.
>
> In which case, maybe that core can (must?) be kept pure and isolated from
> typical real-world developers.
>
> br
> Paul
>
> [1] http://deepspec.org
> [2] https://lists.trustable.io/pipermail/trustable-software/2016
> -July/000005.html
>
> _______________________________________________
> trustable-software mailing list
> trustable-software at lists.trustable.io
> https://lists.trustable.io/cgi-bin/mailman/listinfo/trustable-software
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.trustable.io/pipermail/trustable-software/attachments/20170205/094f5b06/attachment.html>


More information about the trustable-software mailing list