From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,55ae3803eb91d6ca X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news2.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post01.iad.highwinds-media.com!newsfe04.iad.POSTED!7564ea0f!not-for-mail From: "Michael" Newsgroups: comp.lang.ada References: <355dc49a-3414-4883-a268-fa3bcc493e7b@o11g2000yql.googlegroups.com> Subject: Re: Ada UK conference: SPARK safety: is no delivery better than 1 defect? X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5512 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.5579 Message-ID: <62pvl.120778$EO2.21395@newsfe04.iad> NNTP-Posting-Host: 174.6.150.104 X-Complaints-To: internet.abuse@sjrb.ca X-Trace: newsfe04.iad 1237196034 174.6.150.104 (Mon, 16 Mar 2009 09:33:54 UTC) NNTP-Posting-Date: Mon, 16 Mar 2009 09:33:54 UTC Date: Mon, 16 Mar 2009 02:18:09 -0700 Xref: g2news1.google.com comp.lang.ada:4139 Date: 2009-03-16T02:18:09-07:00 List-Id: "Ludovic Brenta" 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.