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: donh@syd.csa.com.au (Don Harrison) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/18 Message-ID: X-Deja-AN: 257533404 Sender: news@syd.csa.com.au X-Nntp-Posting-Host: dev50 References: <33CC0548.4099@flash.net> Organization: CSC Australia, Sydney Reply-To: donh@syd.csa.com.au Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-18T00:00:00+00:00 List-Id: Sorry for taking a while to get back to you.. Ken Garlington wrote: :Don Harrison wrote: :> :> Ken Garlington wrote: :> :> :Don Harrison wrote: :> :> :> :> If even this small overhead is unacceptable, you can force static binding :> :> where necessary by freezing routines. :> :> Although you forgo the flexibility of :> :> polymorphism, you can still take advantage of inheritance by virtue of Eiffel :> :> synonyms - these allow you to declare a routine under different names. :> : :> :But I can do this in Ada, as well, so I don't see the benefit. :> :> I'm not saying there is any extra benefit - merely that you don't have to :> wear the overhead of dynamic binding if you're desperate to maximise efficiency. :> Tucker mentioned that overhead. I'm saying it isn't an issue. : :But you also said that it was required to use that part of Eiffel :inheritance not :available in Ada. No, you've misunderstood. What I'm saying is: 1) If you want to forget about using polymorphism in Eiffel, you can force static binding by freezing features. This prevents you from redefining that feature in a descendant. 2) However, if you want to leave open the possibility of redefining you can call a feature by two names - do_something and frozen_do_something. This allows you to use frozen_do_something in all calls (thus forcing static binding) and still be able to redefine the feature via the other name. (See my previous post for the example of "equal" and "frozen_equal"). Whether or not you can acheive the same thing with tagged types and renaming I wouldn't have a clue. :In this statement, you seem to be saying that if I :want an :efficient safety-critical system (which I always do), I have to give us :some of :that extra inheritance. Not inheritance but polymorphism. : Do I need the full Eiffel inheritance model, or :don't I? Probably not - don't know. :> BTW, how do call a procedure under different names in Ada? : :Via the "rename" statement. : :> :> : :Does this "pre-allocated memory pool" mean that you will know exactly :> :> :what address :> :> :each object's data will reside at, or merely that you dynamically :> :> :allocate memory :> :> :at initialization and do not dynamically allocate after initialization :> :> :is complete? :> :> :> :> The latter. You don't actually need to know *where* objects are allocated, :> :> merely that there is sufficient memory to allocate them. :> : :> :Actually, in my systems, I do need to know where they are allocated, so :> :that :> :I can examine them from the hideously crude display in the cockpit :> :during :> :troubleshooting. :> :> That *is* hideously crude (and brings back some bad memories). Depending on how :> crude you mean, maybe a primitive tool could give you a map of where objects get :> put in memory. If you mean incredibly crude, use non-reference (expanded in :> Eiffel) types and use a linker-generated memory map. : :Both approaches require that the memory address be known before :execution time, :however, so I still care where objects are located. I also care for :other reasons, :such as memory-mapped I/O, of course. Yes. :> :> 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. : :This is why my blood pressure goes up! Well, this was naive of me wasn't it? In mentioning the very word "Ariane" a thousand assumptions come flooding into some people's minds about what you are implying. I was implying nothing - just responding to your request for an example of a high level assertion. I did not intend to imply any deficiency of Ada in this or anything else that you may have assumed. 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. :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! Yes. :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). Not a good assumption. :The other part of the problem was that the _response_ to the assertion :violation was :wrong. The designer assumed the assertion would occur due to a hardware :failure, not :a software requirements failure, and so the handler shut down the :"offending" hardware, :rather than attempting some other action (e.g. replacing the :out-of-range value with :a "safe" value).. Clearly, the assumptions weren't properly thought out. Getting them right would have made the difference. :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. 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. 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. :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. :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. :> 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? :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. :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. :What standard (DO-178?) did you use for certification? Which is?.. :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. :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. :> 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. :> :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. :> :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