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

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

"Ludovic Brenta" <ludovic@ludovic-brenta.org> wrote in message 
news:355dc49a-3414-4883-a268-fa3bcc493e7b@o11g2000yql.googlegroups.com...
>I read your post three times and I still can't figure out what your
> point is.
>
> You claim that "iFACTS has failed as an engineering results" >
> --
> Ludovic Brenta.

Hi Ludovic,

Made it "CAATS" and you get what Nav Canada is reporting in its latest 
Operation Strategic Plan. section - 08T.4, page 53.
http://www.navcanada.ca/ContentDefinitionFiles/Publications/CorpPublications/AdditionalPublications/Ops_Strategic_Plan_2008_2011_en.pdf

The media is the message.  It's a short message, but the audience is its 
contents. (McLuhan http://www.youtube.com/watch?v=RtycdRBAbXk).

Nav Canada is not the problem.  Like almost Praxis, Nav Canada just has no 
solution to a specific engineering problem.

The common denominator:  both assumed being able to undertake a project far 
beyond their usual level of expertise and capabilities.

Behind the iFACTS or CAATS delays and deficiencies is a "Correctness by 
construction" complex: quite the saint Bernard (Madoff) syndrom: "providing 
the latest and most up-to-date "world class" tools available", continuously 
underestimating risks, overestimating self-confidence, great lack of global 
vision.
There is no cure for that.

Such syndrome is even contagious if engineers fail to answer.
(Engineers are trusted. Therefore they should avoid fooling themselves to 
preventing fooling others.)

Instead the engineer reactions went on the autopilot: so we adjusted the 
level of effort according to the level of difficulties until we get out of 
resources.

The problem: we can get far, even too far:
e.g.:  During their training, during CAATS integration and while in charge 
of flight traffic control, the air traffic controllers get progressively 
caught within the system verification.  At the beginning they get the 
deficiencies we identified and resolved but didn't have time to integrate, 
then the one we had identified but not resolved yet, and then others we 
might have anticipated, but not yet identified.
The system was hardly converging to a compliant solution, but confidence's 
up and down increased the inertia.

The response time due to such inertia was critical: i.e.: Reactions were 
pending until it's almost too late.

http://www.navcanada.ca/ContentDefinitionFiles/Publications/CorpPublications/AdditionalPublications/Ops_Strategic_Plan_2005_2008_en.pdf - 
nothing yet about CAATS deficiencies..

http://www.catca.ca/English/Association_Minutes/May7-07.doc, page 2, A10
(QM is Moncton, QX Gander, QG Winnipeg, UL Montreal ACC)

http://www.catca.ca/English/Branches_and_Facilities/BF-May24-07.html
(St-Laurent Region Branches and Facilities: Montreal ACC)

http://www.navcanada.ca/ContentDefinitionFiles/Publications/CorpPublications/AdditionalPublications/Ops_Strategic_Plan_2007_2008_en.pdf, 
page 41 - 2005-2008 OSP is updated

A question : what has triggered the controller reaction : the cumulative 
error effect or the error amplitude?

By using Ada as a formal language to address the increasing dependence of 
complex engineering systems on software; by better evaluating and reducing 
risks to an acceptable level, from almost all of the following:
 - Using proven procedures in dealing with problems
 - Using experience and knowledge of the fact to make decisions
 - Having a well-thought-out process that utilises careful advance 
preparation
 - Providing stability, consistency, predictability and efficiency
 - Considering the reality of the situation

Answer: That issss.. the error amplitude.
Why: Deficiency impacts remain unpredictable even after an anomaly is 
identified.

CAATS is a $1 billion Ada project that is currently operational within 6 of 
7 ACCs. Not all deficiencies are actually resolved, but CAATS safety might 
be likely improved depending on the way priorities are perceived.

By using formal methods' proofs as an abstract certitude of future 
correctness.

Answer: that is the cumulative error effect.
Why: Real world's anomalies don't get easily identified until the final 
trial. And you might not realize what you are doing until all is done right, 
but not necessarily the right thing.

Therefore, iFACTS is safe since it doesn't work, but that is not sufficient. 
i.e.: iFACTS is a required safety component which should already being 
reliably working.
From that point of view, formal methods' proofs are much better!

Cheers

Michael,
Vancouver, BC


Did I miss something?

Real world is not mathematically perfect.  Safety is almost based on the 
robustness to unexpected events, and on the perception and/or control of 
anomalies or errors: e.g.: numerical error from computer's calculation, 
digital signal conversion, measurement precisions, error processing 
(handling, tolerance), system recovery, interface with system at risk of 
deficiencies, different mathematical approximations eventually according to 
transposition within different specific application domains, ., and the 
unforeseen interactions between any of the above, scattered across more than 
one system, at different system levels.

In comparison, the defect Tokeneer caught is a trivial abstract case of 
range overflow.  By specifying a range, this defect can get caught from 
boundary testing or SPARK data flow analysing.

"System stability is based on the notion that one change will not cause one 
or more problems shortly after that change is made. In fact, the system 
should go from one stable state to another to another. Such stability needs 
to be system-wide, not just as applied to one sector, so that changes made 
by one operator will be consistent with the needs of other operators. One 
aspect of conflict detection which does not change is the role of the 
operator as being in control and responsible." Nav Canada

"I am very optimistic about the future. With an air safety regime that is 
already among the best, our commitment to safety and to promoting a stronger 
safety culture will help to maintain Canada's position as a world leader." 
Transport Canada's "Dear Minister"

If any claim: Canada is not in the Somerset.