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.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC autolearn=no 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: JP Thornley Subject: Re: Need help with PowerPC/Ada and realtime tasking Date: 1996/05/30 Message-ID: <292872602wnr@diphi.demon.co.uk>#1/1 X-Deja-AN: 157673361 x-nntp-posting-host: diphi.demon.co.uk references: <63085717wnr@diphi.demon.co.uk> <31AC0712.29DF@lmtas.lmco.com> x-mail2news-path: relay-4.mail.demon.net!post.demon.co.uk!diphi.demon.co.uk organization: None reply-to: jpt@diphi.demon.co.uk newsgroups: comp.lang.ada Date: 1996-05-30T00:00:00+00:00 List-Id: In article: bobduff@world.std.com (Robert A Duff) writes: > I suppose it depends on your definition of "correct". The > proof-of-correctness folks define "correct" to mean "correctly obeys the > formal specification". To me, that's a bogus definition. In plain > English, a "correct" program is one that does what it's supposed to do, > regardless of whether the specification is wrong. If you show me a word > processor that deletes my file when I told it to italicize a word, to > me, that's incorrect, even if you can show me a (bogus) formal spec that > says that the "italicize word" function should delete files. I'd be more impressed by this argument if the examples (such as this and "safety-critical green") were more realistic. [But see below] If you > show me a flight-control program that crashes airplanes, that's > incorrect IMHO, despite the fact that you might show me a formal spec > saying it did what the formal spec says. > OK, a slightly better example (I assume that you don't mean that the requirement has a 'crash plane' operation). But how does this point of view influence the production of the code that implements the requirements (other than by asking the software engineer to be aware of possible errors and omissions and looking out for them - a point that has already been covered in these discussions). There seem to be three main software engineering steps to implementing safety-critical code. 1. Examine the requirements and satisfy yourself that they are acceptable. 2. Implement the requirements as specified (a *correct* implementation). This process can bring out further anomalies in the requirements. 3. Identify any additional potential failures that have been introduced by the implementation and deal with them (either at the software or the system level). For example how do you recognise and deal with corruption of data stored in RAM. If you demand a correct/safe implementation in code of a flight control system from requirements that are incorrect/unsafe then what steps would you take to achieve it? -- ------------------------------------------------------------------------ | JP Thornley EMail jpt@diphi.demon.co.uk | ------------------------------------------------------------------------