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: 103376,59dddae4a1f01e1a X-Google-Attributes: gid103376,public From: "Kevin F. Quinn" Subject: Tasking in safety-critical software (!) (was Re: Need help with PowerPC/Ada and realtime tasking) Date: 1996/05/28 Message-ID: <31AAE196.1438@banana.demon.co.uk> X-Deja-AN: 157137865 x-nntp-posting-host: cdc.demon.co.uk references: <1026696wnr@diphi.demon.co.uk> <122916091wnr@diphi.demon.co.uk> content-type: text/plain; charset=us-ascii organization: Computing Devices mime-version: 1.0 newsgroups: comp.lang.ada x-mailer: Mozilla 2.0 (Win16; I) Date: 1996-05-28T00:00:00+00:00 List-Id: JP Thornley wrote: > > Richard Riehle writes: > [well argued case for tasking mostly snipped] > Several studies into safety-critical subsets have all rejected tasking:- > Safe Ada > SPARK Ada > High Integrity Ada Study (YSE/BAe) > CSMART Ada > so there is going to be a major credibility problem convincing a > qualification authority to go along with tasking. > > Allow also for the relevant personnel from that authority to have an > unknown level of mathematical and computer system literacy. It's worth noting at this point, that IME even the majority of software engineers have difficulty with the complexity of proving things about systems using tasks, in anything but the most trivial of cases. Especially given that there's little or no tool support. And the reason there's no tool support (i.e. the reason why tasks are excluded from those subsets) is that it's mathematically complex, in the extreme, to perform automated proofs. Many language features are excluded from those subsets largely on grounds of being difficult to analyse, rather than any inherent danger from dynamic behaviours. > > A cyclic executive does not guarantee schedulability. It does not > even > > guarantee predictability. In fact, a cyclic executive can guarantee > > that one actually fails to trap events as they occur. > > But safety-critical systems I'm talking about have *no* interrupts (see > my original response - perhaps not sufficiently emphasised) so this > argument does not apply. (Actually there is one - the timer that drives > the minor cycle - and this has to be explicitly justified in the safety > case.) Agreed. The cyclic executive _can_ be used to guarantee schedule periods. In a real-time, safety critical system, a major part of the various analyses performed are to prove termination of a subprogram, and in the case of real time applications to prove upper limits on execution times. This enables worst-case schedule times to be proven to a high level of confidence. Of course, essentially the cyclic executive approach takes control away fro the "black box" tasking system, and places control explicitly throughout the application, which helps one to "know" what's happening at various points. > > An additional problem with the cyclic executive model is ist lack of > > portability. Since it is dependent on the timings of the platform > to > > which it is targeted, it can fail to meet its goals when ported to a > > new platform. > > Agreed - any hardware or software change that affects the timing > analysis means that you have to do it all again, and you may have to > redesign the schedule. (But if it comes to a trade-off between safety > and portability there's not much doubt as to which way I'd go.) Portability is largely a non-issue, w.r.t. safety critical software, IME. As you say, any change in hardware necessitates large volumes of analysis to be performed again. Another point is that when hardware changes substantially (e.g. processor "upgrade", possibly the only real case where portability would be useful) then the opportunity is often taken to implement additional requirements that mean large-scale modifications to the software anyway. > > .... Remember that I speak here of Ada 95 tasking. > > I was beginning to wonder whether I was the only reader of cla still > using Ada 83 until there were some recent posts from others in the same > situation in another thread. Reading this group does, IMO, give a false impression as to the market penetration of Ada95, certainly in the defence industry. Large sections of the industry are still only vaguely aware that it even exists as a standard, let alone that GNAT is now an almost complete implementation. Certainly most people I work with (and have worked with), who work with Ada every day, know little or nothing about GNAT. Another issue is that the sort of projects we're talking about have long development periods, of the order of many years, and of course Ada95 compilers don't have anything like the maturity of existing Ada83 compilers. Having said all that, it'll be interesting to see whether GNAT gets used in very safety-critical systems. All the source-code analysis in the world won't help in the slightest if the compiler isn't correct - and with commercial compilers the best you can expect to get is some kind of statement from the vendor as to the correctness of the compiler. Ada95 does have the extra pragmas to assist in object-code verification, but with GNAT, you have the complete source code to the compiler - something commercial compiler writers are unlikely to release, so there are possibilities for actually including the compiler itself into the proofs. Not that I'd relish the task of proving much about the compiler, of course :) Hmm; that's quite enough for now... Kev. Speaking for (and no doubt to ;) ) himself.