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,193117a6843a81b2 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news1.google.com!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!pd7cy1no!pd7cy2no!shaw.ca!pd7urf2no.POSTED!53ab2750!not-for-mail X-Trace-PostClient-IP: 70.79.99.242 From: "Michael" Newsgroups: comp.lang.ada References: <9f80aed6-6509-4faf-931b-e05dc2b314d9@59g2000hsb.googlegroups.com> Subject: Re: SPARK User Group 2008 X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.3138 X-MIMEOLE: Produced By Microsoft MimeOLE V6.00.2900.3198 X-RFC2646: Format=Flowed; Original Message-ID: <2WD0k.488$i01.271@pd7urf2no> Date: Sun, 01 Jun 2008 20:47:58 GMT NNTP-Posting-Host: 64.59.144.74 X-Complaints-To: abuse@shaw.ca X-Trace: pd7urf2no 1212353278 64.59.144.74 (Sun, 01 Jun 2008 14:47:58 MDT) NNTP-Posting-Date: Sun, 01 Jun 2008 14:47:58 MDT Organization: Shaw Residential Internet Xref: g2news1.google.com comp.lang.ada:508 X-Original-Bytes: 7656 Date: 2008-06-01T20:47:58+00:00 List-Id: "Stuart" wrote in message news:483d26f5$1_1@glkas0286.greenlnk.net... > "Michael" wrote in message > news:ZCY_j.169009$rd2.39062@pd7urf3no... > > must do better! > Stuart Right Stuart you had the point: you extended the safety view, but stuck on details and get mixed up. >From that view, you could almost tell that the Praxis Correctness by Construction formal methods are incompatible with a software-intensive safety-critical large-scale system like NERC. (Please, don't confound with the formal methods, (from engineering control theory); which provide mathematical guarantee of the modeled system's behaviour in the presence of state and input constraints. e.g.: design of multi-objective control laws that by construction will guarantee stability, and prevent input saturation.) Praxis CbC formal methods are mathematical abstractions transposed within the software development domain (i.e.: Z, SPARK). The intents are to enhance reliability by verifying coherence of specifications, code semantic correctness and resilience to dataflow defects. Such CbC set of principles, distilled from formal methods, (like he said), should have been diluted within some engineering crystal-clear water. That would have prevented Praxis-HIS to drive iFACTS crazy - as well as most of his engineers - quite probably. NATS's NERC was developed by Lockheed Martin, in Rockville, MD. After some adaptations in the UK (e.g.: problems with 0 degrees longitude, and so on ...) NERC went solid like a rock - finally. iFACTS is almost plug and play (Lockheed Martin enhanced the NERC interfaces accordingly). iFACTS successful development announcements were interrupted soon after March the 7th 2007. Indeed soon after iFACTS hit NERC at the NATS final trial, (probably, just by the time Praxis-HIS consults his formal specifications and tried to figure what could have happened?). A solution: keeping the rock and getting a new Ferry (rock proof)? Praxis-HIS probably didn't yet realize it should be more cost and time effective if Lockheed Martin were restarted the job, but in a compatible NERC Maryland style manner - (i.e.: SEI CMMI level 3 or higher). iFACTS development is following an old predictable pattern (e.g.: SEI CMMI - between level 1 and 2). i.e.: Increasing the divergences without addressing deficiencies, delays or reducing risks, that is not an innovation. ATC projects are all interconnected. Better to keep that on track, like that: http://www.bcferries.com/about/super_c_tracker.html) NERC using Praxis' iFACTS is composing one hybrid system made from hybrid technology and hybrid development process and methods. It is increasingly common to see safety risks arising from the unforeseen interactions of reliable sub-systems. Get a problem. On which of these sub-systems a correction can be applied? Consider both systems can have a few intrinsic defects. (One more than the other). Knowing one dysfunction, can you retrace the related deficiency by following the anomalies across different conceptual models? You would have to continuously transpose your finding from one model to the other, and reciprocally. (Worst: software development environments have not to be compatible. Problem solving tools either. Easy to get caught by a lot of non related points - depending of the size of the views, they might look weird, but are not necessarily related to any anomaly). Stuart, you already get mixed up by the transposition of a simple lack of visibility (iFACTS lack of testing vs. misuse of Ferry equipment). Ada wrote an application without a target to apply. Later, it worked! iFACTS conceptual methods are also about math! Never heard of the Laplace transform? - Application domains and purposes are different, but one corollary is the same: an error made in one domain can hardly bee seen in the other, but within the applications' results - i.e.: quite too late). Please, would you be kind enough to report your finding to Praxis-HIS. They might appreciate your support. (i.e.: While completing SHOLIS, they perceived a few of the limitations for more complex projects. Whether they didn't remember or wanted a second opinion). >From another hands, Praxis-HIS inappropriately promotes HIS High Integrity Software capability by emphasizing the SPARK approach to safety and security. Better to say, "SPARK suits for writing programs that need to be reliable, and thus particularly relevant to those applications areas where safety and security are important." (John Barnes) Reliability is based on the probability an item will perform its required function in the specified manner over a given time period and under specified or assumed conditions. Beyond reliability, safety is not exactly a SPARK capability. Safety is a planned, disciplined, and systematic approach to preventing or reducing accidents throughout the life cycle of a system. That requires getting the global safety picture (even the configuration data). "Too narrow, a view of architecture will lead to a very pretty infrastructure, but the wrong infrastructure for the problem at hand". (Grady Booch) "The safety risk associated with a complex software-intensive system is a dynamic property that could easily vary with modifications to the system or changes to the operational environment. Mechanical, electrical, chemical and many other engineering disciplines have well established approaches for managing safety risk. However, the increasing dependence of complex systems on software control has fundamentally changed the source of safety risk for such systems." Engineering is not an exact science. There is no simple solution. Safe systems require time, effort, special engineering knowledge and experience. Like it said, the SPARK Praxis-HIS approach has still that advantage: It didn't made iFACTS reliable, but safe since iFACTS can't be used. Assuming another safety risk is just a matter of not delaying for long some Medium Term Conflict Detection capabilities within NERC. Cheers, Michael, Vancouver, BC THE POINT: "It is not enough to talk about "absolute safety" and of "zero accident". There must also be proper organisation and management to ensure that actions live up to words." (UK Department of Transport) iFACTS didn't go strait to this point! Praxis-HIS is not even pretending he could! For satisfying DoT, an US detour seems appropriated. http://www.praxis-his.com/pdfs/cost_effective_proof.pdf http://www.anthonyhall.org/html/papers_on_formal_methods.html