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-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!l12g2000yqo.googlegroups.com!not-for-mail From: Martin Newsgroups: comp.lang.ada Subject: Re: OT?: AF 447 and avionics software Date: Sat, 6 Jun 2009 10:34:57 -0700 (PDT) Organization: http://groups.google.com Message-ID: <3d6ecae8-8a48-4070-acd4-bec9d2d073b7@l12g2000yqo.googlegroups.com> References: <78pifuF1k9uvuU1@mid.individual.net> <96c44af9-d16d-45fb-b264-c77e0ec127a0@x3g2000yqa.googlegroups.com> NNTP-Posting-Host: 86.148.100.105 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1244309698 9776 127.0.0.1 (6 Jun 2009 17:34:58 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 6 Jun 2009 17:34:58 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: l12g2000yqo.googlegroups.com; posting-host=86.148.100.105; posting-account=g4n69woAAACHKbpceNrvOhHWViIbdQ9G User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.0.10) Gecko/2009042315 Firefox/3.0.10, Ant.com Toolbar 1.3,gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:6339 Date: 2009-06-06T10:34:57-07:00 List-Id: On Jun 4, 7:20=A0pm, roderick.chap...@googlemail.com wrote: > 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= an > > > article where an 'expert' questions "damn computers". Particularly th= is > > > quote: > > > > "In these fly-by-wire systems, one never really knows if one has chec= ked out > > > all possible combinations of events to make sure that the computer pr= operly > > > reacts," > > > >http://www.time.com/time/world/article/0,8599,1902421,00.html > > > > Frankly I know nothing about the aviation standards for software/comp= uter > > > use, but I suspect it is somewhat more strict than "one never really = knows". > > > I mean, surely you can't test everything, but I guess one can be reas= onably > > > 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= not > > > sure there's really verified reasons to point to it yet but, trying t= o stay > > > on topic: > > > > I think Airbus is mainly Ada, right? Do you know some good place to r= ead > > > about its software systems? > > > > What about these ADIRU units, are they delivered to Airbus by some pr= ovider > > > 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. > > =A0- Rod Chapman, SPARK Team Sorry, I wasn't trying to imply that SPARK was used in this case - just an example of a tool that is available and could be used in such systems. I have no idea if PolySpace or a PolySpace-like tool is used either. I would doubt they only do dynamic testing. Cheers -- Martin