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.3 required=5.0 tests=BAYES_00, 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: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/19 Message-ID: <33D17AE1.4B42@flash.net> X-Deja-AN: 257786473 References: <33C835A5.362A@flash.net> <33CC0548.4099@flash.net> <33CD578D.562CC6A4@munich.netsurf.de> Organization: Flashnet Communications, http://www.flash.net Reply-To: kennieg@flash.net Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-19T00:00:00+00:00 List-Id: Joachim Durchholz wrote: > > Ken Garlington wrote: > > > You would use them anywhere that a piece of code makes assumptions. > > For example, > > > to help avoid the Ariane fiasco, include contracts in the INS(?) > > that specify > > > Ariane 4 dynamics. Then, in testing, you will get an assertion > > violation when > > > you apply Ariane 5 dynamics to it. > > > > This is why my blood pressure goes up! > > > > The _Ada_ implementation did generate an assertion violation the very > > first time > > Ariane 5 dynamics were applied to it. Unfortunately, the very first > > time > > Ariane 5 > > dynamics were applied to it was at LANUCH! > > > > They were not applied earlier, because the contractor assumed that the > > Ariane 5 > > dynamics were the same as the Ariane 4, so why spend the money testing > > to the same > > conditions already tested earlier? (They were wrong, of course, but > > they > > didn't know > > that at the time). > > that misunderstanding again. The issue in the Ariane-5 paper by > Meyer and Jezequel isn't that the preconditions per se would have > changed anything. Actually, they base the claim on three possibilities, although they immediately withdraw one (assertion performance during execution). In addition to the documentation benefits, they state: "Assertions (preconditions and postconditions in particular) can be automatically turned on during testing, through a simple compiler option. The error might have been caught then." There are several flaws with this statement, which I have addressed previously. However, since you have agreed that this would not have changed anything, I'll skip the analysis of this point. > The issue is that the preconditions would have been an > integral part of the routine's signature, and thus not likely to have > been overlooked by the team that ported the Ariane-4 code to Ariane-5. There are several flaws in this statement. Since I have addressed them before in detail, I will summarize them now. 1. There is no evidence that the right precondition (which is not a simple precondition) would have been inserted in the code even using DBC. (There is not necessarily a simple correlation between the flight profile and the HZ variable in question.) 2. There is no evidence that the reviewer would have had access to the Ariane 5 flight profile data necessary to detect the precondition violation. (The final report notes that the data was withheld intentionally, with concurrence at several levels. Without this data, the reviewer would have been assured that the problem could not occur.) 3. There is no evidence that, if inserted, it would have been reviewed by a system engineer, or someone else with the ability to correlate the flight profile with the HZ range. (The final report implies that the system specification or a "justification document" might be a more logical place, and that a special team be generated to review these documents.) 4. There is no evidence that, if inserted, the precondition violation would have been manually detected amongst the sea of other preconditions that would have to be manually checked. (The final report makes note of the complexity of the system and the difficulty of such analyses, and recommends several other items, such as realistic testing, to compensate for this difficulty.) > As it were, the preconditions were buried in some obscure part of the > documentation, and management didn't reread everything when they reused > the code (together with its hardware). > > The paper may not be very clear in this respect (I got Meyer's view on > the topic from his book, not from the paper), or people might > misinterpret what it's saying. I don't misinterpret it at all. I merely note that, _in this case_, there is no evidence it would have changed anything. > > According to Meyer, et. al. Eiffel programmers would have written the > > handler > > differently, and also they would have known to do the testing > > differently (even though > > the requirements specification said that the tests need not change). > > No. They would have written the handler the same way, and documented the > precondition with the routine where it belongs, not in some obscure spec > sheets that are shelved away. Interesting, because the final report notes quite explicitly that the handler was also a source of the error: "Although the source of the Operand Error has been identified, this in itself did not cause the mission to fail. The specification of the exception-handling mechanism also contributed to the failure." Thus, if _any_ of the four points above apply, then the results would have been the same. Meyer's paper makes no mention of the exception handling approach defined for DBC; thank you for clarifying this. > > > However, their > > explanation as to why this is true is far from convincing (basically, > > that "Eiffel > > programmers believe in quality" or some such nonsense). > > Well, believing in quality is far from nonsense. And assertions do > certainly promote a certain style of quality-mindedness. > It is similar to declaring types for routine parameters. Early C didn't > have them, current C compilers have them. And besides catching lousy > errors, the need to declare parameter types makes the programmers > *think* about what's the right type for a parameter, instead of just > writing it down. A similar mechanism is at work with assertions and > Eiffel programmers. The "nonsense" is that Eiffel programmers have a corner on such thinking. Meyer's paper states that "The ESA's software people knew what they were doing and applied widely accepted industry practices" (the latter half of this statement is contradicted by the final report), but then goes on to say "Any team worth its salt would have checked systematically that every call satisfies the precondition." Such a statement is hopelessly naive, as noted above: there are several factors that would have worked to defeat the best-intentioned review team. None of these are addressed in the paper (or afterwards). > > > They believe that "software is software." and apply the > > expertise in their > > domain to mine. > > Well, their finding may have been badly presented, but I think the > "software is software" approach is valid. Of course there are > differences between various levels of safety requirements, An internally contradictory statement. Can you define these differences, and explain why they are not a potential factor for this subject? > but some > basic themes apply all the same - like static typing, or the need to > choose meaningful names, etc. Meyer believes that assertions should be > considered one of these basic themes, and that assertions might have > prevented the Ariane-5 crash, for the reasons given above. (And I'm very > much with him, though I'm not informed enough about the Ariane-5 crash > to decide wether it is a particularly good example of the issue.) I think you've put your finger on it. People who are Meyer fans, but not particularly well informed on the Ariane 5 issue, believe Meyer. People with experience in these kinds of safety-critical systems do not, at least from what I can tell. Furthermore, there is no evidence that the paper was even reviewed by someone on the Ariane 5 team, or even someone with a background in such systems, prior to its publication. I always thought peer review was an essential part of any scholarly paper. Note that your statement is wrong, by the way. I could forgive Meyer to some extent if he had said that assertions "might" have prevented the Ariane-5 crash. He goes much further: He states that they "probably" would have avoided the crash. Such a statement carries with it a much stronger proof requirement, which he fails to provide. > > > I am aware of at least one project developing an embedded missile > > controller, > > that did exactly what you describe (in Ada). Here's what happened: > > > > 1. Their timings changed, which introduced some subtle differences in > > the > > relationships between tasks and external interrupts. Some of these > > subtle > > differences invalidated their original testing. > > Timing on that basis is the one thing that Eiffel isn't built for. > Adding a new class might not change subtle timings, it might totally > alter the microscopic behaviour of the program. For example, > non-polymorphic routine calls that could be statically bound by the > compiler might become polymorphic and required a dynamic dispatch. > Fine-tuning code so that certain routines are guaranteed to take at > least x ms and at most y ms sounds to me like a very difficult and > fragile thing to achieve in Eiffel. It is a difficult and fragile thing in any language, and best avoided. More to the point, it is important in testing to look for such fragile dependencies (race conditions & deadlock in particular). This testing cannot be done on code with significantly different timing properties than the production system. > > > 3. At least one compiler bug was introduced, which was definitely > > unsettling. > > That's a problem of compiler quality. Eiffel doesn't guarantee perfect > compilers, but assertions should make bugs less likely. I presume you mean assertions in the compiler, since obviously the assertions can't be relied upon to detect errors in the application at this point. Is there evidence that Eiffel compilers use assertions extensive internally? Is there evidence that, as a result, they have far fewer bugs than other compilers? (These aren't idle questions; if this is the case, this is actually a valid argument for the use of Eiffel in safety-critical systems that hasn't been offered to date.) > > > The other prong of this is that, while assertions are keen for > > catching > > design problems, I haven't seen much evidence that they catch > > high-level > > requirements problems (not surprising, since the code was presumably > > written > > to match the requirements). In 13 years of developing safety-critical > > embedded systems, our process tends to handle design problems fairly > > early. > > It's those high-level requirements problems where we need the most > > help. > > Eiffel is the only language that I know that can scale up to formalizing > high-level requirements. The technique is easy: write a few abstract > ("deferred") classes that aren't much more than a set of routine > signatures and assertions. > One can even implement such a system: Just take the design classes as > ancestors for your implementation classes. Descendants must keep the > assertions, so your code is guaranteed to match the specs (in a way - > assertions aren't statically checked). I am skeptical that Eiffel is a good language for SRSs. Is there any evidence that it has been used this way? Are there issues about the notation being easy to understand by non-programmers? > > > But almost all of our safety-critical threads are hard realtime > > threads! > > That's a HUGE limitation for our systems! > > Well, if you don't have confidence in the compiler, there isn't much you > can do to remove assertions (or run-time range checking, which are a > limited form of assertions). > But in this domain there's no difference between Eiffel and Ada - the > problem's the same, and there is no satisfactory solution available. Exactly. Again, I think you agree with me that the non-documentation aspects of Eiffel assertions can be discounted with respect to the Ariane 5 -- killing two of three of Meyer's arguments. Now, all you have to do is agree with any one of my four points on documentation, and we can put this argument to bed :) I've noticed several times that Eiffel advocates try to make this a langauge debate betwen Ada and Eiffel. I could care less. I've made the same points about Ada that I make about Eiffel. > > BTW I'm somewhat curious how these subtle timing differences come to > have practical consequences. I'm not a hard real-time engineer, so I'd > expect it doesn't matter if a routine runs faster than expected. How > come that your experience is obviously different? > > > What is the process to certify Eiffel compilers as being acceptably > > mature > > (code generation-wise) for safety-critical systems? Is all testing > > performed > > with assertions on and assertions off in all test cases? > > There isn't even a testbed available - probably because nobody earnestly > demanded it yet. This seems odd. If Eiffel compilers use assertions, then why wouldn't the compielr development team, which presumably is "worth its salt," establish the high level of quality you assert is the province of all Eiffel programmers? Why would someone need to "demand" a means to measure and improve the quality of the toolset? > > > However, what about the topic of this thread (safety-critical > > systems)? > > It sounds > > like there's a lot of limitations as to using (and inheriting) > > assertions for > > this environment. > > I think OO in general is difficult to apply here. I'm not convinced of this, BTW; I have seen at least object-based safety-critical real-time systems operate quite nicely. I have also seen some features of OO not found in object-based designs (e.g. full polymorphism) used on mission-critical real-time systems, and I expect that we will use at least some of this in our future safety-critical systems. > You obviously need > tight control on the code generated, to control the timings. A good > Eiffel compiler will do a global analysis of the system and apply > inter-routine optimizations. This makes the type of control you desire > difficult, and I'm not sure wether the better reliability is worth the > price. Ada compilers do extensive inter-routine optimizations in our safety-critical systems. Again, you misunderstand: it's not that the object code is complex; it is that the object code tested needs to be the object code delivered. > > > > :Of course, Bertand Meyer's Eiffel website insists that even > > > :misinterpretation of > > > :requirements (Ariane V) will be a problem no longer when Eiffel is > > used! > > > > > > Come on. He's not saying that. > > > > Read his analysis of Ariane V. He says _exactly_ that, and has > > defended > > saying that in multiple newsgroups. A smart person, but not someone > > who knows my domain particularly well. > > The Ariane-5 crash wasn't a requirements misinterpretation. It was > overlooking a part of the requirements. To quote directly from the final report: "it is even more important to note that it was jointly agreed not to include the Ariane 5 trajectory data in the SRI requirements and specification." I know that Meyer's report makes no note of this fact (it would weaken his argument considerably if he did!). This is why you need to read the final report for yourself and compare it critically to Meyer's interpretation, as I did. Even without a background in this area, you should see some contradictions. Meyer, in fact, says: "The requirement that the horizontal bias should fit on 16 bits was in fact stated in an obscure part of a document.", but the final report says something a little different: "...three of the variables were left unprotected. No reference to justification of this decision was found directly in the source code. Given the large amount of documentation associated with any industrial application, the assumption, although agreed, was essentially obscured, though not deliberately, from any external review." This quote refers to the deliberate decision by the Ariane 4 designers to _not_ state this requirement (more importantly, not to _handle_ the case in the code in the right manner) which, ultimately, caused the failure. How Meyer got his statement from this, I have no idea. Don't take my word for it (or Meyer's!): read the report at: http://www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html > > Regards, > Joachim > -- > Please don't send unsolicited ads.