Re: Certified C compilers for safety-critical embedded systems

From: Robert I. Eachus (rieachus_at_comcast.net)
Date: 01/10/04


Date: Sat, 10 Jan 2004 01:16:07 -0500

Larry Kilgallen wrote:

> From another point of view, they just opened the system testing process
> up to the public view :-)

Sorry, no. If the course of Ariane 501 would have been slightly
different, the launch would have succeeded. But it would have said
nothing about the likelihood that then next Airiane 5 launch would have
succeeded. In fact there have been three major failures in less than a
dozen launches, with lots of originally needed testing done after each
failure, and they still don't have a working system. In the meantime,
Ariane 4 (Remember, the one the software requirements were originally
for?) has had about 100 launches with a very good record.

So the Ariane 5 is almost the poster child for doing reuse without
redoing the systems requirements analysis from the top. I would hope
that no one would ever make that mistake again. But the lesson that
keeps being taught about the first Ariane 5 launch is about software
validation.

Similarly the lessons learned in five Airbus 320 crashes are getting
papered over. It is by now clear to those who study such accidents,
that all five accidents were probably caused by invalid requirements.
For years Airbus has claimed that the software had been proven correct
and couldn't have caused the crashes. But finally enough has come out
that the accident investigators are pretty sure they know exactly which
requirements error caused which crash.

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.

-- 
                                           Robert I. Eachus
"The war on terror is a different kind of war, waged capture by capture, 
cell by cell, and victory by victory. Our security is assured by our 
perseverance and by our sure belief in the success of liberty." -- 
George W. Bush


Relevant Pages

  • Re: Certified C compilers for safety-critical embedded systems
    ... the launch would have succeeded. ... Ariane 4 (Remember, the one the software requirements were originally ... that all five accidents were probably caused by invalid requirements. ... For years Airbus has claimed that the software had been proven correct ...
    (comp.lang.ada)
  • Re: EELVs: Time to Pull the Plug
    ... >>These fixed costs are part of the Titan IV number ... > as well as maintain a launch capability of Ariane V of a dozen a year (even ... > to 2-3 Ariane V lanch a year without some serious reductions. ... substantial cost when it comes to DoD launch support. ...
    (sci.space.policy)
  • First Ariane launch of 2006 (Forwarded)
    ... satellites into geostationary transfer orbits. ... The Ariane 5's cryogenic, liquid fuelled, main engine was ignited first. ... fraction of a second after that, the launch vehicle lifted off. ... 33850 km/h) and the conditions for geostationary transfer orbit injection ...
    (sci.space.news)
  • Ariane 5 -- second launch of six in 2007 (Forwarded)
    ... an Ariane 5 ECA launcher lifted off from Europe's Spaceport ... This second launch of the year keeps Arianespace and Europe's Spaceport on ...
    (sci.space.news)
  • Re: Europe to Join Russia in Building Next Space Shuttle
    ... >> Here, elucidate us, Monsieur Mezei: ... >> that would have to be made to carry Columbus on Ariane V. ... > While it's certainly true that there's no way to launch truss segments ... > with ATV I'm not so sure about Columbus. ...
    (sci.space.shuttle)