Re: Ada UK conference: SPARK safety: is no delivery better than 1 defect?

["Michael" <fvit@shaw.ca>]

Hi Bill and all,

iFACTS has failed as an engineering results. Engineers are used to find 
solutions rather than excuses (i.e.: former SPARK successful software 
development process involves substituting testing by formal proofs; and the 
iFACTS managers were confident that proven procedures were used in dealing 
with problems.  In case of problem, changing the way engineering must be 
done is a necessity for engineers to report).

Tokeneer is an open project, so open for discussion:

My initial question was: "In regards to the Tokeneer mini-project findings, 
were the safety critical iFACTS project's delays and deficiencies 
predictable?"

A few months prior NATS realised iFACTS was ending with a lot of 
deficiencies, Praxis and NATS were still celebrating a great iFACTS success 
story (just prior the final iFACTS trials at Hurn).

"Paul Barron, NATS' Chief Executive commented: "This is one of the most 
exciting developments in the aviation industry in decades and we're now 
close to introducing it."

http://www.praxis-his.com/news/radarmar2007.as
http://www.nats.co.uk/uploads/user/NERL%20Business%20Plan%20Report%202008.pdf 
page 6

"In all engineering disciplines it is accepted that it is better to avoid 
the introduction of errors rather than have to correct them at a later 
stage."

How "correctness per construction" fails to meet such a fundamental goals?

Pre-condition: there must have no effective validation or verification 
procedure.

It might be a few known limitations: e.g.: SPARK can ensure intrinsic code 
robustness, but not the software compliance toward system specifications.

But there if were enough deficiencies to avoiding iFACTS to converge to a 
compliant solution, there were enough for SPARK to catch. And SPARK, as well 
as that the Z formal specifications, caught none of them.

What's the SPARK problem?  Good enough for Tokeneer, blind as a bat for 
iFACTS!

The next Ada UK Conference is still a responsibilities for Rod Chapman and 
Janet Barnes to clarifying the Praxis's SPARK capabilities (Tookeneer) and 
limitations (iFACTS).
In 2007, conclusion of  "Correctness by Construction: Putting Engineering 
into Software" was quite amazing:
http://www.adacore.com/multimedia/aa_videos/lectures/adauk07_05_slides.pdf
 "A future?
     What happens if we put together:
        - ...
        - CbyC,
        - SPARK and strong static verification,

     Don't know! But we aim to have some fun finding out."

Have fun,

Cheers

Michael,

Vancouver, BC

CC: to Rod Chapman and Janet Barnes


Just in case:

Formal specifications can describe in a precise way the properties of an 
information system, but without constraining the software architecture and 
design in which these properties are to be achieved.  In others word formal 
specifications describe what the system must do without saying how it is to 
be done.  Therefore, formal specifications are the mathematical foundation 
which can ensure system requirements shall be transformed into consistent 
and accurate systems specifications.

The general goal of SPARK is to provide a language which increases the 
probability of the software code behaving as intending.  In another word 
SPARK provides additional information, which allows performing rigorous 
mathematical analysis in order to significantly increase the code intrinsic 
integrity and runtime correctness.  The benefits are to reduce the risk of 
processing erroneous data, and then preventing any error handling and/or 
system recovering risk, ultimately preventing system instability, saturation 
or even crash.