Re: Certified C compilers for safety-critical embedded systems

["Alexandre E. Kopilovitch" <aek@VB1162.spb.edu>]

I think that the following posting (of Robert I. Eachus) should be placed in
appropriate section of Ada-promoting websites, at least unofficial ones, such
as AdaPower and AdaWorld - because it is the best explanation of the Ada
adavantages at essentially popular level I ever seen. Yes, it may be enhanced
by correcting typos (I noticed at least one) and by making the explanations
of the crash cases slightly more detailed (perhaps providing simple pictures)
- not all readers have pilot experience or at least are regular readers of
Flying magazine; but even without those enhancements it is a very rare writing,
which can explain the matter for some people inlvolved into decision processes
about software - so it should be made easily accessible and referenced.


> Date: Sat, 27 Dec 2003 16:33:47 -0500
> From: "Robert I. Eachus" <rieachus@comcast.net>
> Subject: Re: Certified C compilers for safety-critical embedded systems
> To: comp.lang.ada@ada-france.org
> Message-ID: <0ridnTmiEKohZ3Ci4p2dnA@comcast.com>
>
> Alan Balmer wrote:
> 
> > That seems obvious. It's possible to write a C program with *no*
> > residual errors. It may be easier to write a SPARK program with no
> > residual errors, but there's no law that says C programs have to have
> > more errors.
> 
> But is it possible to write a C program and an Ada program which 
> implement the same algorithm with no residual errors?
> 
> My experience indicates that it is not.  This is not saying that you 
> can't build an Ada to C translator, or a C to Ada translator, although 
> the first has been done several times, and the second would be much 
> harder.  The problem is that if I have a C program "in hand" and go to 
> translate it into Ada, there are usually hundreds of questions that I 
> end up asking.  Some of them may be answered in the specificiation for 
> the C program--assuming that such a specification exists.
> 
> The net result is that even if I start out to write identical programs 
> in C and Ada, the Ada program ends up much more tightly specified. 
> Whether these additional specifications are meaningful in terms of the 
> intent of the program, or are just "accidental" overspecification due to 
> the fact that Ada asks the question and it is easier to answer it than 
> dodge it, the Ada and C programs implement two different specifications. 
>   (Or to be formal, the set of specifications that the C program 
> satisfies will normally be a superset of those satisfied by the 
> "equivalent" Ada program.)
> 
> Does this make the C program better?  I don't think so.  I am much more 
> concerned that set of specifications satisfied includes the "real" 
> specification, which often includes requirements omitted from the 
> original written specification.  Ada does a much better job of 
> identifying these implicit requirements and getting them formalized.
> 
> The best example of this problem doesn't involve Ada at all.  The French 
> developed a programming language used for the Airbus A320, and it took 5 
> crashes for omissions in the specification to be identified and fixed.
> 
> One problem was that the autopilot would maintain a specified hight 
> above ground between waypoints until the last waypoint before landing. 
> Then it would put the plane into the glidepath for the destination 
> runway.  The problem occurred when the last waypoint set was not in the 
> glide path, the 'correction' that occurred when the waypoint was passed 
> could result in a stall, or in the case of a landing in mountainous 
> territory diving to the glide path which was underground at the last way 
> point.
> 
> Airbus originally diagnosed the cause of the crashes as the pilots 
> selecting the 'wrong' descent mode.  But as I said, it was not pilot 
> error, but a missing specification.  The glide path for the runway was 
> assumed to be everywhere above ground.  More correctly it was assumed 
> that the last waypoint would be the outer beacon for the intended 
> runway.  But there are cases where that is not possible, and in those 
> cases, the A320 could be deadly. And in the crash which resulted in the 
> problem being detected, the outer marker beacon was situated on a 
> mountain which extended into the glide path.
> 
> As far as I am concerned Airbus's contribution to the analysis of a 
> crash near Strasbourg, France January 20, 1992 was criminal.  If you 
> look at all the "weasel words" in retrospect, they knew that it couldn't 
> have been the pilot error they suggested.  (Autopilot in wrong mode.) 
> The "rapid" descent that left one second between the altitude warning 
> and the crash was at over a 50% angle over descending terrain.  Somehow 
> I don't think the flight crew "overlooked" the rapid descent--other than 
> looking through the cockpit window below their feet.
> 
> As it was, it took two more crashes before an investigation concluded 
> that at least two previous crashes, and probably all four were due to 
> missing requirements in the specifications for the provably correct 
> code.  For example, in the first crash at a French airshow, a lot of 
> attention was focused on whether the engines spooled up "quick enough" 
> when the crew selected abort/go around.  A later crash in Japan in a 
> similar situation, but a "real" landing attempt showed that engine speed 
>   wasn't the problem.  The Japanese plane didn't strike trees with its 
> tail: "Finally, the engine stalled after the angle of ascent increased 
> to 53 degrees, and the plane fell towards the ground, crashing 
> tail-first."  As any pilot can tell you trying to increase altitude in 
> any flight mode, but certainly when close to the ground, pulling the 
> nose much above level is a deadly error. Beyond a certain AoA (angle of 
> attack) the plane will slow down requiring more AoA (or throttle) to 
> stay level. Go back and look at the first A320 crash, and it is clear 
> that a human pilot would have not have increased the AoA to go around, 
> and in (more) level flight the tail would not have hit the trees.
> 
> Sorry to spend so many electrons and photons on this, but it is an issue 
> that should not be overlooked.  Formal proofs of correctness are 
> worthless if the requirements are not complete.  I like a language that 
> asks the questions that the specification forgot.
> -- 
>                                            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