Re: OT?: AF 447 and avionics software

[Martin <martin.dowie@btopenworld.com>]

On Jun 4, 7:20 pm, roderick.chap...@googlemail.com wrote:
> 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

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