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-Thread: a07f3367d7,7c1ca6be7961c074 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!x3g2000yqa.googlegroups.com!not-for-mail From: roderick.chapman@googlemail.com Newsgroups: comp.lang.ada Subject: Re: OT?: AF 447 and avionics software Date: Thu, 4 Jun 2009 11:20:51 -0700 (PDT) Organization: http://groups.google.com Message-ID: <96c44af9-d16d-45fb-b264-c77e0ec127a0@x3g2000yqa.googlegroups.com> References: <78pifuF1k9uvuU1@mid.individual.net> NNTP-Posting-Host: 217.205.167.137 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1244139651 9236 127.0.0.1 (4 Jun 2009 18:20:51 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 4 Jun 2009 18:20:51 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: x3g2000yqa.googlegroups.com; posting-host=217.205.167.137; posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB; rv:1.9.0.10) Gecko/2009042316 Firefox/3.0.10,gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:6265 Date: 2009-06-04T11:20:51-07:00 List-Id: On Jun 4, 12:02=A0pm, Martin wrote: > On Jun 4, 10:29=A0am, "Alex R. Mosteo" wrote: > > > > > I'm sure most of us are following the news on this issue. I just read a= n > > article where an 'expert' questions "damn computers". Particularly this > > quote: > > > "In these fly-by-wire systems, one never really knows if one has checke= d out > > all possible combinations of events to make sure that the computer prop= erly > > reacts," > > >http://www.time.com/time/world/article/0,8599,1902421,00.html > > > Frankly I know nothing about the aviation standards for software/comput= er > > use, but I suspect it is somewhat more strict than "one never really kn= ows". > > I mean, surely you can't test everything, but I guess one can be reason= ably > > confident on the system design! > > > Now, there's a trend forming pointing to the ADIRU [1] unit, because of > > recent incidents like the Qantas flight mentioned in the article. I'm n= ot > > sure there's really verified reasons to point to it yet but, trying to = stay > > on topic: > > > I think Airbus is mainly Ada, right? Do you know some good place to rea= d > > about its software systems? > > > What about these ADIRU units, are they delivered to Airbus by some prov= ider > > or are of their own built? > > > [1]http://en.wikipedia.org/wiki/Air_Data_Inertial_Reference_Unit > > They can analysis code to ensure absense of runtime error (e.g. using > SPARK and/or tools like PolySpace) but testing all possible scenarios > is a different kettle of fish all together. This is not entirely true. There is certainly SPARK code in the Rolls-Royce engines that power the A380 and Boeing 787. There is no SPARK in the other major avionics systems on the Airbus A320, A330, A340 or A380. (After all, if Airbus were a SPARK customer I would know for sure!) Airbus have cited the use of Patrick Cousot's ASTREE tool in the analysis of their flight control codes - this is published somewhere, so I'm sure a quick google search will reveal the correct ref. - Rod Chapman, SPARK Team