[SystemSafety] Bursting the formal methods bubble

Derek M Jones derek at knosof.co.uk
Wed Oct 25 18:23:57 CEST 2017



Martyn,

> We can't go on for ever building software with a test-and-fix approach
> to assurance. NIS and GDPR (and the HSE OG) may be the comets that
> finally kill the dinosaurs.

Software engineering has a dead body problem:
http://shape-of-code.coding-guidelines.com/2009/11/18/where-are-the-dead-bodies/

> 
> Martyn
> 
> 
> On 25/10/2017 16:10, Derek M Jones wrote:
>> Martyn,
>>
>>> The NSA concluded that Z/SPARK CorrectbyConstruction beat every other
>>> software development approach they had experienced. Search for Tokeneer
>>> on line.
>>
>> My searches only located congratulatory statements by the usual
>> suspects.
>>
>> Is their an internal report that you know about (it was your company
>> that did the work, after all)?
>>
>> Those involved seem to make a big thing about only two bugs being found.
>> One possible reason for such a small number of bugs is that very few
>> people used the software in anger.
>>
>> This work found new 20 problems, of which half could lead to
>> system failure:
>> www.open-do.org/wp-content/uploads/2010/04/ERTS2010_final.pdf
>>
>>
> 
> 
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> 

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


More information about the systemsafety mailing list