Certified C compilers for safety-critical embedded systems - Page 9

Do you have a question? Post it now! No Registration Necessary

Translate This Thread From English to

Threaded View
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Grin.

Well in C you can have signed char where char'Pos is range -128 .. +127 and
unsigned char where char'Pos ist 0 .. 255. One of the top 10 mistakes K&R
did. It leads to a lot of misunderstandings and signed char is only used
when Short_Short_Integer is needed.

Which is yet another example where in C you have to say "A" when realy you
want "B". How a static analysis tool will deal with this I never know.

With Regards

Martin

--
mailto:// snipped-for-privacy@users.sourceforge.net
http://www.ada.krischik.com


Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

->savety<-

Quoted text here. Click to load it



Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Cleanup in Aisle 7.

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

And in many buildings, the next higher floor after 12 is 14.
In my building, the next higher floor after 14 is PH.

If anything, counting in the real world is a lot like Ada
enumeration types.


Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

And it is, generally using binary...

Counting in the _source_ of computer programs should be done in the
way to maximize correctness of the computer-human interface.  For
the number of people who attended a Modern Western Square Dance,
that means starting at 8 (any fewer and there was no dance).

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Please, there is a version of GNAT that requires zero run-time support.
   In fact in the safety critical market it is favored as a base for
SPARK, since then there is no need to validate the run-time.

But remember that you really have to think in terms of development host,
target, and the ICE or other system used to download and run tests.  So
the triplet you want may or may not be supported.

Quoted text here. Click to load it

There have been several Ada compilers that targetted 8-bit
microprocessors.  However, I don't think anyone ever validated an 8051
target due to capacity limitations.  There is an interesting discussion
here, at length, about that topic (in 1995):
http://www.adahome.com/News/Trip-Reports/TA95-email.html

There is evan a comment there (by me):

"AFAIK the smallest computers that Ada has been targeted to
include the 128-kbyte Western Digital P-machines, the Russian PDP-11
clones, and the RRSoft compiler which ran on 512K 8088 based
PC-clones.

However, in all these cases the compiler was self-hosted!

So certainly an 8051 target is very reasonable, it just remains
to be seen if anyone wants to do it."

I think the situation is still the same, although there are other 8-bit
and even 4-bit microcontrollers with Ada targets.  So it may just be
that programmers who choose Ada choose Motorola microprocessors, and
vice-versa.  (In point of fact, I've never used an Intel microprocessor
in an embedded system, but I have used many Motorola chips, and Z-80s.)

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Exactly my point. A theoretically good language is useless without the
support tools.... And those support tools haveto be of high quality as
well.

Quoted text here. Click to load it

I am surprised.

Quoted text here. Click to load it
That is the problem. A non-validated Ada compiler would be no more value
than a good C compiler. Actually  a good C compiler eg the Keil C51 that
has been extensively used in safety related projects by a large number
of people would be better simply because of the empirical field usage
compared to a non-validated Ada compiler with a small user base..


Quoted text here. Click to load it


That takes some doing!!!


Quoted text here. Click to load it

I doubt it. At least not in large enough numbers to justify it
especially as 61508 permits C  (subset, with coding standard and static
checking) to SIL-4

In effect a SPARK-C


Quoted text here. Click to load it

Yes there are a LOT!!  They are mainly the 186 and 386. There are of
course the PC 104 systems but... Strangely due to the sort of projects
they 186 and 386 were used in there has been a lot of activity in that
field over the last 9 months.... However I doubt this interest will
continue (unless somewhere else gets invaded)



/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England    /\/\/\/\/\
/\/\/ snipped-for-privacy@phaedsys.org       www.phaedsys.org \/\/
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

When you says static checking, do you include static checkers that can prove
that assertions are never volilated (within a set of assumptions)?  If so
then your C subset with static checking might be in effect a SPARK-C.  SPARK
supports some very nice formal verification techniques which you might be
overlooking.

-CRM



Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

No. I was thinking about Lint initially but I am sure that some of the
better (more expensive :-) tools will test to various criteria etc and
AFAIK do what you are suggesting but I am not certain on this.  any one
using QAC or LDRA's tool like to comment?

/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England    /\/\/\/\/\
/\/\/ snipped-for-privacy@phaedsys.org       www.phaedsys.org \/\/
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

I'd like to hear your thoughts on the noted 100:1 residual error
improvement between SPARK code and C code, all DO-178B level A.  Do
you think the C code examined did not use "a subset, coding standards
and static analysis"?  If they didn't, who does?  Is your claim that,
properly used, C can yield equivalent residual error rates as SPARK?
If so, why do you think the code examined in the study was a 100 times
worse?

Mike

Re: Certified C compilers for safety-critical embedded systems
On 24 Dec 2003 14:59:57 -0800, snipped-for-privacy@yahoo.com (Mike Silva)

Quoted text here. Click to load it

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.

Quoted text here. Click to load it
Hard to tell, from the given data. Direct access to the study would be
needed. I would be surprised if the authors of the study didn't do
some analysis of causes.

--
Al Balmer
Balmer Consulting
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

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,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

I had a thought about this also.  In the Ada case we see a change from
R (recommended) to HR (highly recommended) at SIL3 and SIL4.  In the C
case we see a change from NR (not recommended), past - (no
recommendation) and R to HR.  To go from Ada to SPARK is one step
(i.e. good to best) while to go from C to SIL4-C is three steps (i.e.
worst to best).  How will that (3 step improvement vs. 1 step
improvement) manifest itself in the complexity, cost and lack of
errors in the tools, the expressiveness and ease of use of the
resulting language subset, etc, etc.

Mike

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

btw not "worst to best"  

I agree to a point. I think this reflects the engineering profession is
maturing and the support tools are coming of age.

Quoted text here. Click to load it

I think that there are now tools and methods in place that there were
not previously.  The sheer weight of the commercial pressure has
improved quality in the compilers and support tools. It has generated a
lot of safety related support for a language that was not originally
designed to be a safety critical language.

This does not mean it can't be used for safety related projects just
that initially the users were not working in that sort of a field so the
mind set was not there. You could write appalling code in Ada but the
average practitioner has been taught Ada with a view to safety related
systems. The majority of C programmers were not.



/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England    /\/\/\/\/\
/\/\/ snipped-for-privacy@phaedsys.org       www.phaedsys.org \/\/
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Re: Certified C compilers for safety-critical embedded systems
Several people have asserted the argument that the large
number of users of a given tool implies quality in that tool.

I don't buy it.  By this logic, MS Windows should be
absolutely flawproof, and the infamous Pentium Divide bug
should never have happened.

No amount of usage can make up for design flaws.  Popularity
is much less about technical qualities than it is about
marketing.  C, Windows, x86 chips have substantial market
share, which is not the same as saying that they have
substantial quality by design.

            dave



Re: Certified C compilers for safety-critical embedded systems
writes
Quoted text here. Click to load it

We are in comp.arch.embedded...... Ms Desktop tools are not relevant.
Besides AFAIK their license excludes any safety critical use.

Quoted text here. Click to load it

Correct for the desktop tools but among *Embedded* tools it does
especially where the aim is to go for the high reliability market.

/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England    /\/\/\/\/\
/\/\/ snipped-for-privacy@phaedsys.org       www.phaedsys.org \/\/
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Some of us are in comp.lang.ada.

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

Repent!
:-)
/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ Chris Hills  Staffs  England    /\/\/\/\/\
/\/\/ snipped-for-privacy@phaedsys.org       www.phaedsys.org \/\/
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

How do you think I got *into* comp.lang.ada?!

Quoted text here. Click to load it

Me too!

Re: Certified C compilers for safety-critical embedded systems

I would much rather concentrate on technical issues here (for example,
why deep static analysis of _any_ general-purpose langauge is
impossible; or, why systems of integrities in the better-than 10e-6
failures per hour class _require_ deep static analysis); however, I
can't let Chris Hill's petulent little rant below pass unchallenged!

Chris Hills wrote:
Quoted text here. Click to load it

Praxis has a long-held commitment to using the best technology available
and to advancing the state of the software industry as a whole.  Our
objection to using C for SIL 4 is that it is unsuited to that task.  The
majority of the proponents of the use of C in this role are C tool
vendors; are they too governed only by vested interest?

Quoted text here. Click to load it


Neither slide is erroneous. They are clearly dated 2002 and are factually
correct for that date.  We had two members on the original MISRA-C
committee
and attended every workshop and committee meeting until the beginning of
this year.  We still monitor the mailing list and will contribute again
when
we have something to say.

Quoted text here. Click to load it

Wrong.  We did.  Unfortunately the rather stern view we took of what was
needed to make C fully-analyseable (basically, a Pascal subset in C
syntax) was not seen as being compatible with the apparent aim of the
comittee: as much C as possible with the minimal restrictions needed to
plug the biggest holes.

Quoted text here. Click to load it

The slide clearly states that this is Rod's personal view and he (with
appalling semantics) qualifies the "unique" with "almost".  I think is
is at least defensible to say that Praxis's experience as: implementors
of world class critical systems, language designers; and tool vendors
_does_ give us a different (even unique) perspective from most other
contributors none of which (AFAIK) has done _all_ of these things.

Quoted text here. Click to load it

Perhaps you can recall the context in which Less Hatton's shack/swamp
comment can be interpreted in a positive way?

Quoted text here. Click to load it

We don't rubbish C.  We rubbish magic where logic is to be preferred.
We have well-articulated reasons for saying that C is not well suited
for constructing high-integrity systems.  The proponents of C for this
purpose never seem to present their reasons.  All we ever hear are:
"there are lots of C programmers around"; "we only ever employ the best
people and they don't make those kinds of mistakes"; and, the falsehood,
"C, with suitable support tools, is as good as anything else".

We don't take this view because we have alternative tools, we have
alternative tools because we take this view!

Quoted text here. Click to load it

Again we are not trying to rubbish MISRA-C.  We continue to believe that
  it is useful enterprise.  If people want to use C for smaller,
safety-related systems then having a widely-supported coding standard is
a "good thing".  We will continue to rubbish the promotion of that
coding standard to application domains for which it unsuitable.

We no longer promote a MISRA-C tool because the widely-differing
behaviour of our and competing tools and the high level of ambiguity in
the MISRA-C rules showed that the market was too immature for tools
claiming to enforce MISRA-C compliance.  We preferred, in that
situation, to say nothing rather than make claims that could not be
defended by logic and by reasoned argument.  I hope that MISRA-C2 will
be  better; however, my long experience of designing unambiguous and
analyseable programming languages leads me to believe that it won't.

Quoted text here. Click to load it

Fundamental misconception.  SPARK is wholly unambiguous and therefore
analyseable in a formal and mathematical sense.  An un-annotated subset
of C _cannot_ have this property.  Analysis of such a language can,
therefore, ony result in the _detection_ of certain kinds of error, it
cannot _prove_ that they have been eliminated.

Quoted text here. Click to load it

Use, even widespread use, does not imply suitability.

Quoted text here. Click to load it

Agreed.  Modula-2, in particular, was a nice language from which a
secure, SPARK-like sublanguage could have been constructed.  Pity it,
unlike Ada, never achieved critical mass.

Quoted text here. Click to load it

I have pooh-poohed this pooh-poohing enough already!

Quoted text here. Click to load it

have a Happy New Year


Peter


Site Timeline