[SystemSafety] Collected stopgap measures (Hoare)

[Nick Tudor]

Thanks Rod for citing Typhoon PFCS as an exemplar.  The Release to Service
of that software was supported by independent formal proof of all 350,000
SLoC from 2003 up until 2007.  This was done initially by DERA (then
QinetiQ) led by Colin O'Halloran and his Systems Assurance Group in Malvern.

Nick Tudor
Tudor Associates Ltd
Mobile: +44(0)7412 074654
www.tudorassoc.com

*77 Barnards Green Road*
*Malvern*
*Worcestershire*
*WR14 3LR*
*Company No. 07642673*
*VAT No:116495996*

*www.aeronautique-associates.com <http://www.aeronautique-associates.com>*


On Fri, 16 Nov 2018 at 10:54, Roderick Chapman <
roderick.chapman at googlemail.com> wrote:

> On 16/11/2018 10:31, Martyn Thomas wrote:
>
> Echoes of the great Tony Hoare: How Did Software Get So Reliable Without
> Proof? <https://www.gwern.net/docs/math/1996-hoare.pdf>
>
> There are plenty of examples (including those cited by Paul) of software
> which has evolved ultra-reliability (and some concensus of "requirements")
> over
> decades, with hundreds of releases and millions of users.
>
> At the other end of the spectrum, we build systems that have to be
> demonstrably fit-for-purpose at the point of first deployment.
> You get one release and no chance of patching... Typhoon PFCS is an
> obvious example, but I'm sure there must be lots of others.
>
> Paul - how would you go about building and justifying such a system?
>  - Rod
>
> _______________________________________________
> 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/20181116/2f2f37e6/attachment-0001.html>