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: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: Joachim Durchholz Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: <33CD578D.562CC6A4@munich.netsurf.de> X-Deja-AN: 257710871 References: <33C835A5.362A@flash.net> <33CC0548.4099@flash.net> X-Priority: 3 (Normal) Organization: ccn - computer consultant network GmbH Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: 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. 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. 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. > 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. > 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. > 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, 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 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. > 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. > 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). > 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. 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. > 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. 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. > > :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. Regards, Joachim -- Please don't send unsolicited ads.