[SystemSafety] Collected stopgap measures (Hoare)

[Nick Tudor]

Yup, all of it, PFCS, auto-throttle, auto-pilot....the lot.....  DERA
started with 18,000 SLoC in 2001/2 and showed the manual code was well
above 'world class'....but still found some issues.  This took one year
elapsed time and 6 man/years.  The techniques were refined and used on
various iterations, eventually doing all 350,000 SLoC in 4 man months, 2
months elapsed, one month of which was writing the report.  The problem
space became well known and we built tools to increasingly automate
verification, but NB this was then a highly tuned verification tool suite
to that particular problem and practitioners that understood it.
Specifically, we developed a highly tuned proof automation process; the
effort was in setting up the refinement in the first place and no manually
directed proofs were eventually required.  The process/tools can no longer
be used ( I think the code is now written in C and not Ada) .......among
one or two other issues.

Note that the code was already very, very high quality; probably among the
best on the planet at the time, so this was a massive bug hunt looking for
the odd infraction across lots of documentation covering specification and
code; some were found of various levels of 'seriousness'.  It was
eventually decided that there was no longer as much benefit to be had in
doing the independent work as the code base was not changing as much, the
core functionality, in particular, was fixed and hence the bang for the
buck was no longer justifiable.

Incidentally, I was impressed by the 18KLoC stage, so (in my RAF days) I
set up a 3 month experiment in 2003 based on using an autocoder instead of
manual coding with both the developer and DERA.  The focus was on a few
functionally significant modules of the 18KLoC.  After fixing a few
misunderstandings (on both sides), all autocode was proven to implement the
module specifications and furthermore, they all passed the existing unit
tests that had been developed for the manual code.  While there were timing
issues in some modules, the principles were established, which was the
point of the experiment (there were routes to making the code more
efficient (optimised) which have been developed and can maintain the
automatic proof).  Measurements of effort were also taken and, while there
are various interpretations of the results, the outcome was that (shock)
the autocode and the proof process, even with [well qualified] people
involved, there were considerable savings to be had, while maintaining
integrity.

There used to be some papers on this, but I now longer have access to
them.... :-(

Hope that helps...have a good weekend

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 13:48, Derek M Jones <derek at knosof.co.uk> wrote:

> 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
> _______________________________________________
> 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/ea172be8/attachment-0001.html>