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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-Thread: f849b,b8d52151b7b306d2 X-Google-Attributes: gidf849b,public X-Google-ArrivalTime: 2004-01-10 06:30:59 PST Path: archiver1.google.com!news2.google.com!fu-berlin.de!news.eunet.no!uninett.no!news.net.uni-c.dk!sunsite.dk!newsfeed1.uni2.dk!news.get2net.dk.POSTED!53ab2750!not-for-mail Newsgroups: comp.arch.embedded,comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems References: <3fe00b82.90228601@News.CIS.DFN.DE> <5802069.JsgInS3tXa@linux1.krischik.com> <1072464162.325936@master.nyc.kbcfp.com> <1563361.SfB03k3vvC@linux1.krischik.com> <11LvOkBBXw7$EAJw@phaedsys.demon.co.uk> <3ff0687f.528387944@News.CIS.DFN.DE> <1086072.fFeiH4ICbz@linux1.krischik.com> <3ff18d4d.603356952@News.CIS.DFN.DE> <1731094.1f7Irsyk1h@linux1.krischik.com> <3ff1b8ef.614528516@News.CIS.DFN.DE> <3FF1E06D.A351CCB4@yahoo.com> <3ff20cc8.635997032@News.CIS.DFN.DE> <40000150.3050305@noplace.com> From: Mark Lorenzen Message-ID: User-Agent: Gnus/5.1002 (Gnus v5.10.2) Emacs/21.3 (gnu/linux) Cancel-Lock: sha1:eMzH85ve0P3O3yT7EYcBR2R3N9g= MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Fri, 09 Jan 2004 06:13:38 +0100 NNTP-Posting-Host: 62.84.221.216 X-Complaints-To: abuse@colt-telecom.dk X-Trace: news.get2net.dk 1073745058 62.84.221.216 (Sat, 10 Jan 2004 15:30:58 CET) NNTP-Posting-Date: Sat, 10 Jan 2004 15:30:58 CET Organization: Colt Telecom Kunde Xref: archiver1.google.com comp.arch.embedded:7224 comp.lang.ada:4306 Date: 2004-01-09T06:13:38+01:00 List-Id: Marin David Condic writes: > It would seem intuitively obvious to even the most casual observer > that if you're not sure what a thing is *supposed* to do, you can't > possibly be sure that it does it. Unfortunately, this lesson is often > learned at great financial (and sometimes human) expense. > > MDC Indeed. I am a big proponent of formal methods and mathematical proofs. But using these tools makes it even more important to get the requirements correct, sound and complete. - Mark Lorenzen > > Robert I. Eachus wrote: >> The Airbus 320 should bury the idea that theorem provers can result >> in safe software. In the case of the Airbus 320 what happened was >> that the formal logic used for stating the requirements/theorems was >> relatively opaque to experts in the field (read pilots). So the >> flaws in the requirements, and later about 500 people, were buried >> by that opacity. >> > > > -- > ====================================================================== > Marin David Condic > I work for: http://www.belcan.com/ > My project is: http://www.jsf.mil/NSFrames.htm > > Send Replies To: m o d c @ a m o g > c n i c . r > > "Face it ladies, its not the dress that makes you look fat. > Its the FAT that makes you look fat." > > -- Al Bundy > > ======================================================================