Re: OT?: AF 447 and avionics software

[roderick.chapman@googlemail.com]

On Jun 4, 12:02 pm, Martin <martin.do...@btopenworld.com> wrote:
> On Jun 4, 10:29 am, "Alex R. Mosteo" <alejan...@mosteo.com> 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 this
> > quote:
>
> > "In these fly-by-wire systems, one never really knows if one has checked out
> > all possible combinations of events to make sure that the computer properly
> > reacts,"
>
> >http://www.time.com/time/world/article/0,8599,1902421,00.html
>
> > Frankly I know nothing about the aviation standards for software/computer
> > 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 reasonably
> > 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 to stay
> > on topic:
>
> > I think Airbus is mainly Ada, right? Do you know some good place to read
> > about its software systems?
>
> > What about these ADIRU units, are they delivered to Airbus by some provider
> > 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