[SystemSafety] Collected stopgap measures (Hoare)

Derek M Jones derek at knosof.co.uk
Fri Nov 16 14:47:58 CET 2018


Nick,

> 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

All 350K?  That is rather a lot, normally it's a few thousand lines at
most.  I am asking out of ignorance and surprise.

> 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
> 
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com


More information about the systemsafety mailing list