[SystemSafety] Collected stopgap measures (Hoare)

[Nick Tudor]

Nope, this is formal proof, and nope, it is not marketing...cheeky!  Use of
Z and ProofPower, but, and I will re-emphasise, that the automatic
techniques developed then were highly tuned to this particular problem with
highly skilled people developing the technologies for themselves to use (I
used them.... a bit....; my MSc dissertation in 2000 prior to the
Eurofighter work taking place was on the technique and how to automate
it).  There were marketing types in QQ in 2010 who  thought it could be
applied to any FCS/engine control, etc, but were proved (!) wrong.  We are
now automating it for application to general control systems; size will not
matter, but access to processors (nothing unusual) and some small amount of
time is all that is necessary.

The second question pertains to the automatic aspects used in the
experiment...?.  The line counts per module were generally more than the
manual code (I recall), but by no means all; some were actually smaller.
Most were well within 10% WCET; some, not many, were faster but there were
some outliers that were well over budget. My MSc showed how to make the
problem tractable which generally meant a few more lines of code, more but
significantly easier proofs which meant that the process was automate-able.

Papers were likely within UK MOD...and would have probably involved the
word 'CLawZ'


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

> Nick,
>
> > 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
>
> 18k in 6-man years sounds believable.
>
> > 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
>
> This sounds completely unbelievable.  Or is a marketing definition of
> formal proof being used here?
>
> Was the code automatically generated from a specification containing
> 2-orders of magnitude fewer lines?
>
> > There used to be some papers on this, but I now longer have access to
> > them.... :-(
>
> I can try and track them down, if you have the titles.
>
> --
> Derek M. Jones           Software analysis
> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181116/16ea5aac/attachment.html>