[SystemSafety] This is getting boring (was Re: Number Theorist Fears All Published Math Is Wrong)

[Martyn Thomas]

We have had this sort of debate often on this list and its predecessor.

In my opinion, the core of the argument in favour of the use of
mathematically-based notations, methods and tools ("FMs") is that there
are good theoretical arguments that FMs are far more cost-effective in
reducing a range of defects in software-based systems than the use of
informal notations, methods and tools and that the use of FMs does not
inhibit the parallel use of other methods where they add value.

This argument is strengthened by empirical evidence from a wide range of
projects.

This is not an claim that the use of FMs leads to perfection or to a
guarantee that all defects have been eliminated or that the use of FMs
should be compulsory, especially for systems where safety, security and
reliability are not critically important and where time-to-market may be
an overriding criterion for success.

No complex engineering artefact can be proved free of all significant
defects but engineers in most disciplines have learnt through experience
that it is extremely cost effective to be able to reason about the
critical properties of their designs and products and that mathematics
assists rigorous reasoning.

Software engineers have a diverse range of notations, methods and tools
that they could use for different aspects of their work. When the choice
may affect a critical property of their work, they must be able to
justify the choices they have made.

Martyn

On 01/11/2019 09:09, Peter Bernard Ladkin wrote:

>
> On 2019-10-31 20:53 , Derek M Jones wrote:
>> Claiming to have verified a compiler, when in fact the work only
>> applies to parts of the code generator, is soap powder advertising.
> Yes, but who does this for usable products?
>
> Almost all brief claims are backed up in depth, because anyone who might want to use such a compiler
> likely will have to deal with inspectors and regulators who will not be satisfied with a simple
> statement "We used Company X's compiler which is formally verified" but will want to see appropriate
> V&V.
>
> For example, Ansys says SCADE is "certified to IEC 61508:2010 SIL 3". Even though IEC 61508 makes no
> provision for certification, TÜV Süd has indeed certified it. TÜV Süd/Ansys is happy to tell you
> exactly what that means, namely that there is a certificate on TÜV Süd's letterhead and a detailed
> document available to users explaining exactly what has been verified/validated by TÜV Süd's
> inspection. (Of course, some of it may be hard to fathom, but that is surely to be expected; there
> is no simple recipe book for using sophisticated SW development tools.)
>
> Similarly, AbsInt says "CompCert is a formally verified optimizing C com­piler for safety-critical
> and mission-critical soft­ware" and Daniel Kästner has discussed with me in some detail what this
> means. They have a considerable amount of backing material including tools to help with any use of
> CompCert in the context of DO-178C, IEC 61508 and industry-specific standards.
>
> I'd love to see soap-powder manufacturers take a similar approach to their products. Not that I use
> soap powder.
>
> PBL
>
> Prof. Peter Bernard Ladkin, Bielefeld, Germany
> MoreInCommon
> Je suis Charlie
> Tel+msg +49 (0)521 880 7319  www.rvs-bi.de
>
>
>
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191101/4310048e/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191101/4310048e/attachment.sig>