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-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,abd508cccb4803ea X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2002-06-22 09:47:09 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!bloom-beacon.mit.edu!nycmny1-snh1.gtei.net!cpk-news-hub1.bbnplanet.com!news.gtei.net!howland.erols.net!news-out.worldnet.att.net.MISMATCH!wn4feed!worldnet.att.net!204.127.198.203!attbi_feed3!attbi.com!sccrnsc03.POSTED!not-for-mail Message-ID: <3D14AA34.E8FFBBBB@attbi.com> From: Mark Biggar X-Mailer: Mozilla 4.79 [en]C-{C-UDP; EBM-SONY1} (Win98; U) X-Accept-Language: en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: C.A.R. Hoare on liability References: <3D0E09BA.A492AA3D@despammed.com> <5ee5b646.0206210355.3533be8f@posting.google.com> <3D1390D0.7040709@attbi.com> <5ee5b646.0206220514.55f8cf9a@posting.google.com> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit NNTP-Posting-Host: 12.235.88.57 X-Complaints-To: abuse@attbi.com X-Trace: sccrnsc03 1024764428 12.235.88.57 (Sat, 22 Jun 2002 16:47:08 GMT) NNTP-Posting-Date: Sat, 22 Jun 2002 16:47:08 GMT Organization: AT&T Broadband Date: Sat, 22 Jun 2002 16:47:08 GMT Xref: archiver1.google.com comp.lang.ada:26606 Date: 2002-06-22T16:47:08+00:00 List-Id: Robert Dewar wrote: > > "Robert I. Eachus" wrote in message news:<3D1390D0.7040709@attbi.com>... > > > I agree with the point, but not the example. For Ariane 4, the analysis > > was carried out, and whether or not you agree with the final decision > > for Ariane 4, the decision was well thought out. The disaster was that > > the Araine 4 analysis was carried out absent the Ariane 5 requirements > > for political reasons, and the Ariane 5 requirements analysis was never > > done. > > I disagree. Here you have a case in the Ariane4 code where a check was being > made at runtime which had the quality that if the check failed, disaster > would occur. There are two possibilities > > 1. In the Ariane4 code, it was demonstrated that this check could never fail. > In that case, the check should not have been there. > > 2. In the Ariane4 code, it was NOT demonstrated that this check could > never fail. In that case, they were just lucky that no Ariane4 blew up. > > I will repeat. You should NEVER have a runtime check in your code where it > is the case that failing the check is a more serious situation than not doing > it at all. Casually putting in checks is very likely to generate such cases. > > My understanding of the Ariane case is that this check was casually put in, > in other words it was put in WITHOUT any analysis that said this check was > needed. Deployed code should not have such checks. No the situation was more complicated then that. Ariane 4 had, like most rocket systems, redundant hardware sets each with its own, independent sensor set. Careful analysis was done that showed that given the possible flight profiles, the only way the code should see an overflow was if the sensor suite was packed up and sending bogus data. The check for overflow was thus used to detect hardware problems and the exception raised was to notify the upper control code that that particular hardware set was offline and to ignore it. Ariane 5 had a very different flight profile including much higher accelerations. So when the software was reused, without rechecking the analysis against the new Ariane 5 flight profile, it saw a real overflow that didn't have anything to do with hardware faults, so all the redundent hardware suites overflowed and threw an exception all at the same time. This put the rocket out of control and I believe it was destroyed by the range safety system. So both the check and the exception were reasonable and correct for the Ariane 4 and would not have crashed it. So it was reusing the code without redoing the analysis or even testing it against the new flight profile that cause the problems, not the check in the code. This problem would have arisen regardless of the language used. -- Mark Biggar mark.a.biggar@attbi.com