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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/16 Message-ID: <33CC64CE.44A3@flash.net>#1/1 X-Deja-AN: 257152583 References: <33CBBF4B.7BAF@pseserv3.fw.hac.com> Organization: Flashnet Communications, http://www.flash.net Reply-To: keg0@flash.net Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-16T00:00:00+00:00 List-Id: Don Harrison wrote: > > More than likely the Ariane bug would > have been picked up by traditional means (since it's fairly obvious) but in > the event that it wasn't, it would certainly have been identified if > the assumption was identified and coded as an assertion. ...and the same traditional means (testing to the actual Ariane V data) were used to test the system (otherwise the assertion would never have been exercised). Thus: 1. If the assertion was not identified and coded as an assertion, but traditional means were used, the problem would have been discovered. 2. If the assertion had been identified and coded as an assertion, but traditional means were NOT used, the problem would NOT have been discovered. So, since traditional methods were required anyway, how did adding the assertion (either the Ada "Operand_Error" or your Eiffel equivalent) help for this example? Meyer et. al. argues that, if the system was written in Eiffel, that the assertion would have been added despite the lack of foundation for doing so in the specification, and that reviews of the code would have found the inconsistency between the code and specification, causing the designers to ask the specification writers why they thought the Ariane V profile was the same as the Ariane IV. Thus, even without the testing, the Eiffel system would have uncovered the fault. My argument is that no designer of a non-trivial safety-critical software system could be expected to either (a) have such an all-encompassing knowledge of the total platform to either write or analyze such a complex and subtle assertion or (b) be willing to add assertions willy-nilly with no basis in the specification (extranous code being identified as a potential safety issue in more than one certification scheme). (As an amusing aside, the defenders of the Eiffel faith were reduced to calling my objections "casuistry," or using an inappropriate specific case to prove a general statement. This argument, of course, is using a specific case to prove a _specific case_. One could argue that the Eiffel paper produced by Meyer et. al. was a better definition of casuistry, however!) > > :Or in your own words: > : > :> No use of assertions will stop you misinterpreting requirements. > > True, though irrelevant to the point I wasn't making. :) Not at all irrelevant, unless you claim that assertion writing is not coupled to requirements (which is a very dangerous claim!). If you look at failures in safety-critical aerospace software systems (and I've done more than one study on this), they tend to be requirements-driven (e.g. F-18, YF-22, Gripen, Ariane V). More than one controlled N-version academic study has shown this as well. (One of the best was where multiple teams implemented a set of flight control laws, using a basic safety-critical software development process along the lines of DO-178. There was only one common fault among all of them - a period in the requirements had been misinterpreted as a comma due to the poor quality of the paper version of the control laws!) You could argue that assertions make the process of eliminating design faults easier, thus allowing your finite test time to focus on requirements issues earlier. However, I've talked to people who build safety-critical aerospace systems (and also read Safeware, et. al.) and those kind of issues are usually resolved fairly quickly in *any* good safety-critical software development process. There may be some benefit to assertions in this environment, but it's pretty small when measured against the potential risks. Again, for a non-safety-critical system, where there may be a higher proportion of design faults, then you probably do see a larger benefit (I know I do) for dynamic assertions. For safety-critical systems that can fail-safe, vs. those that must fail-operate, I could also see some benefits (although that class of systems seems to be shirnking every day). However, beware casuistry! :) > > Don. > =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- > Don Harrison donh@syd.csa.com.au