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: 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: Ken Garlington Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/18 Message-ID: <33CFFAF7.6834@flash.net> X-Deja-AN: 257688301 References: <33CC0548.4099@flash.net> 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-18T00:00:00+00:00 List-Id: Don Harrison wrote: > > :> :> Maybe general assertions are more common than you imagine. However, I agree > :> :> that range constraints are roughly covered by Ada subtypes. I use them liberally > :> :> for just that purpose. > :> : > :> :Maybe, but again, I would like to see how these complex assertions are > :> :used. > :> > :> 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. An assertion violation... as in Operand_Error? Again, someone needs to explain how these high-level assertions would have benefitted the Ariane 5 IRS. > So, here's a different example. In my key handling object (one of the highest > level in the simulation), there's an operation for interpreting the CLEAR key. > Simplifying a little, pressing this key should reactivate the menu, clear the > key sequence and clear any menu or sub-menu selection. So, there's a compound > postcondition thus: > > if SA.ASSERTIONS_ON and then (INPUT_STATE /= MENU or else > NO_OF_KEYS /= 0 or else MENU_OPTION_SELECTED or else > SUBMENU_OPTION_SELECTED) then > raise SA.POSTCONDITION_ERROR; > > Note that some of the components are functions. Wrapping them in this way > is typical practice in Eiffel and enables you to use them elsewhere (eg. in > if-statements in the code proper) and makes contracting scalable. In Eiffel, I assume this code would be in the "short form." Is the user/reviewer really expected to read all of this (including looking up the functions embedded in this code) and understand it? Wouldn't it be just as easy to say, in the description of this operation, the English text preceding it? > > Clearly, the assumptions weren't properly thought out. Getting them right > would have made the difference. Keep in mind that the people making these assumptions were not programmers - they were system engineering types. So, unless you propose teaching DBC to all engineers in the program (which might not be a bad idea, actually), then > :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). > > I don't know about you, but I tend to take a pretty skeptical view of > requirements because they often have holes in them. It pays to be a bit > circumspect. Doesn't matter. You (a) would have been told that your suspicions are not a concern, since the Ariane 4 and 5 have the same flight profile, and (b) don't go throwing dumb assertions throughout your code - we're already running around 80% of max throughput! > With regard to whether an Eiffel software engineer would have > picked up the false assumption compared with an Ada SE - possibly, due to the > fact that they are conditioned by their use of contracting to *think* of as > many assumptions as possible so they can code them as assertions. This sort of > conditioning is much less prevalent among Ada developers because most don't > use contracting (in this disciplined sense). I *know* this is true because I > work with them. Of course, they may be (and probably are) more disciplined > in your domain simply because they *have* to be. However, the conditioned > cultural difference due to disciplined contracting would be an advantage. Our engineers are taught the same thing in ADARTS, so I don;t think this is as big a difference as you think. I also challenge whether or not you code all of the assertions you can envision. Look at your example from earlier. There's absolutely no other assertions you could consider? How about the possibility that calling one of the functions in the assertion causes NO_OF_KEYS to become non-zero, just for fun? > For your domain it's a bit of a Catch-22. Contracting would improve the culture > but you're unable to use it due to hard timing constraints. Not at all. We have to distinguish between "contracting" and "assertions." You can still think in terms of writing strong interfaces, with well documented user constraints (ADARTS term), but without coding them. For example, you may write your test cases such that pre-conditions, post-conditions, and invariants are checked outside the object code. You can also permit more comprehensive reviews by documenting them via comments. The point is, you don't have to use DBC/Eiffel to get these benefits... they are also contained in ADARTS/Ada, for example. > > > :However, their > :explanation as to why this is true is far from convincing (basically, > :that "Eiffel > :programmers believe in quality" or some such nonsense). > > No, it's the conditioning that makes the difference. There are a lot of > Ada software engineers who *are* serious about quality (including you, I expect). > Using DBC just makes you more effective. However, the supposed advantage of Eiffel is that this thinking becomes code. I don't see the advantage for my domain (although I certainly do for others). > > :This is why I dislike people with no background in safety-critical > :flight systems discussing > :such issues. They believe that "software is software." and apply the > :expertise in their > :domain to mine. > > Well, having worked in a range of application areas from HRT to 4GL/database, > I can say this is both true and false. What I mean is there are some principles > (eg. how to structure code etc.) that don't change irrespective of whether > you're developing an embedded system or a GUI-based client application on a PC. > There are also things that *do* change. In particular, the options available > to you progressively decrease and the development environment becomes more > hostile as you move further towards the HRT end of the scale (as you know). > > :> :Again, the code I've seen to date doesn't seem to use them that much. > :> > :> If you're looking in Ada code, you're looking in the wrong place because few > :> Ada developers recognise there are additional benefits from using them in > :> addition to static typing and the predefined contracts already in Ada > :> (the conditions under which predefined exceptions - eg. Constraint_Error - > :> are raised). > : > :No - I'm looking at Eiffel code. > > Well, you must be looking in the wrong place. I don't know whether anyone > has given any pointers yet as to where you can find some. Suggestions?.. > > :> Static typing gives you static contract checking. Assertions (predefined and > :> user-defined give you dynamic contract checking *during development*. What > :> most Ada software engineers miss out on is the user-defined variety which > :> bring a non-trivial benefit to reliability and reuse. > : > :Not this Ada engineer! I have dynamic assertions all over the place in > :my > :tools! > > Terrific! > > :My problem, again, is in the fundamental nature of dynamic assertions > :for safety-critical > :embedded systems, which have some unique risks, whether you (a) leave > :them in after development, > > Not recommended for your application area. > > :or (b) take them out after developmental testing, but > :before usage. > > In this case, the software should be regression tested. This requires that _all_ of the testing/analysis be done twice. Putting aside the cost and schedule concerns, any such program will have finite time and other material. I can either do all of this work twice (which dilutes my effort 50%), or I can do it once - which might allow me to do testing that otherwise I wouldn't do. > > :> They are only turned on during development, so what you do is fix the underlying > :> problem which is usually not difficult to find if you've used them systematically. > :> Even if you haven't (I was the only one of a team of 5 using them in our recent > :> development cycle), they still tell you more than you would otherwise be told. > : > :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. > > This is why I have specifically said they *shouldn't* be used in threads where > timing is critical. The fundamental problem is that assertions are executed > *sequentially* and will necessarily affect timing. I haven't thought of any > bright ideas on this one.. > > This is in contrast to GC which can be executed *in parallel* if implemented > on a shared memory - multi-processor architecture. > > :2. Their object code changed (obviously), which required reanalysis of > :their > :object-code branch coverage. > > If assertions are being implemented in a safe way and you can validate that > the compiler is doing the right thing, why should this be necessary? Because structural (path) testing at the object level has been shown to be extremely useful in detecting various types of errors - compiler errors among them. Beizer cites several studies. > > :3. At least one compiler bug was introduced, which was definitely > :unsettling. > > If you really mean a bug (whether from optimisation or something else), this > is not the fault of contracting but the compiler. True, but I have to live in the real world. The families of the people I kill will not be impressed with the statement "That's a tool problem, not a methodology problem." The point is, changing the compiler switches after testing is complete is a Bad Thing. > > :What safety-critical system did you develop where you turned off > :assertions > :afer development? > > None. But if I did, I would regression test to make sure the compiler didn't > stuff things up. Do you run all of your tests, and perform all of your analyses, twice (once with SA.ASSERTIONS_ON set, and the other with it cleared)? Ever miss a schedule date, overrun a budget, or forego any potential testing as a result? > > :What standard (DO-178?) did you use for certification? > > Which is?.. DO-178 is the FAA standard for critical software. It, along with other commonly-used certification criteria, would likely take a dim view of what Eiffel advocates propose with respect to not testing the actual code. > > :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). > > If you're talking about A-specs (specs above the level of Software Requirements > Specs) containing statements like "The Sonar simulation shall simulate > active detection", such requirements are better linked to a bunch of SRS > requirements and checked through them. No, code would usually be written to an SRS. Requirements traceability, while useful, only says that you implemented/tested what was written. It doesn't say that what was written is correct or complete. > > :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. > > Can you give an example? Not sure how high-level you mean. Recent examples: Ariane 5 - incorrect operational profile (Ariane 4 specified instead of 5) See: http://www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html F-18 - divide by zero at Mach 1, due to incorrect control law equation in spec. YF-22, Gripen - PIO due to incorrect control law equation in spec. (PIO is a complex lag interaction between the operator and the system - can't wait to see the assertion for this one!) > :> Yes, timing *is* something to be concerned about when applied to realtime > :> systems. That's why I suggested not using assertions in the hard realtime > :> threads of a process. BTW, software designed using DBC may actually run *faster* > :> than code without it because you get to strip out all the defensive validity > :> checks. You have already ascertained during development that operations are > :> called in valid contexts so you don't have to check the context. > : > :But almost all of our safety-critical threads are hard realtime threads! > :That's a HUGE limitation for our systems! > > Agree. > > :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? > > I am not aware of any use of Eiffel yet for safety-critical systems. What I'm > trying to get across is its *potential* for these systems. That potential > would be contingent on a number of things happening: > > - The addition of a concurrency mechanism. > - The addition of realtime libraries. > - The addition of low-level libraries. > - The addition of a formal certification process for Eiffel compilers. > - A realisation in RT community of the advantages of using Eiffel. Much like saying a brick has the potential to fly... if you strap it to an airplane :) Aren't there more fundamental problems than just this? You state that the assertions can't be executed in a hard real-time thread, so how does a "realtime" library help? > > :> :Another consequence of using assertions is that you have to develop and > :> :test the > :> :assertions. > :> > :> Correct. My initial reaction when I started using them was "Gee, I've got to > :> do this extra work on top of writing the "real" code! However, I found I was > :> spending about a third of the time integrating compared with my colleagues > :> which meant I was saving time overall and producing more reliable code to boot. > :> > :> :As a result, you need confidence that the benefits of the > :> :assertions > :> :outweigh the dilution of your test effort. > :> > :> IME, they do. > : > :However, it sounds like you're talking about a non-safety-critical > :system, and > :certainly not a hard real-time embedded safety-critical systems. In that > :case, > :I agree. For tools, simulations, etc. I would use all of the assertions > :I could. > > Yes, I'm talking about simulators. Our's probably regarded as medium realtime. > > :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. > > In the HRT threads, yes. Elsewhere (not in your case), it is an option. But not all of my issues relate to HRT, so I still don't see that on balance it's a good idea. > :> :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. > > That's probably true. > > Don. > =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- > Don Harrison donh@syd.csa.com.au