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: f849b,b8d52151b7b306d2 X-Google-Attributes: gidf849b,public X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2004-01-10 05:42:45 PST Path: archiver1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!crtntx1-snh1.gtei.net!news.gtei.net!newsfeed1.easynews.com!easynews.com!easynews!elnk-pas-nf1!elnk-nf2-pas!newsfeed.earthlink.net!stamper.news.pas.earthlink.net!stamper.news.atl.earthlink.net!newsread1.news.atl.earthlink.net.POSTED!d9c68f36!not-for-mail Message-ID: <40000150.3050305@noplace.com> From: Marin David Condic User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.0.1) Gecko/20020823 Netscape/7.0 (OEM-HPQ-PRS1C03) X-Accept-Language: en-us, en MIME-Version: 1.0 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> Organization: LJK Software Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Date: Sat, 10 Jan 2004 13:42:44 GMT NNTP-Posting-Host: 165.247.66.40 X-Complaints-To: abuse@earthlink.net X-Trace: newsread1.news.atl.earthlink.net 1073742164 165.247.66.40 (Sat, 10 Jan 2004 05:42:44 PST) NNTP-Posting-Date: Sat, 10 Jan 2004 05:42:44 PST Organization: EarthLink Inc. -- http://www.EarthLink.net Xref: archiver1.google.com comp.arch.embedded:7220 comp.lang.ada:4304 Date: 2004-01-10T13:42:44+00:00 List-Id: 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 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 ======================================================================