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

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
OK


Interesting.... can you explain? Perhaps as a separate thread?

Quoted text here. Click to load it

Is that a contradiction or do you mean that you need static analysis but
it can never be 100%?

Quoted text here. Click to load it
That's got to be from the marketing dept :-)


Quoted text here. Click to load it
On its own I would agree.

Quoted text here. Click to load it

Good point. However you could argue the same for Ada hence the
development of Spark Ada. I think that all that is happening is that
there is (thank god) a realisation that unfettered C *IS* dangerous and
it should be used with various tools not least a static analyser. Who
would buy a word processor these days that does not have a spell
chequer?

Quoted text here. Click to load it
The original committee stopped along while ago.

Quoted text here. Click to load it

That explains why I have not seen any one from Praxis in the last year
or two.


Quoted text here. Click to load it

Can you send it to me? It would be useful to go over it (again?) before
we lock down C2

Quoted text here. Click to load it

Yes. We have to work with the language we have.  Also the view was taken
(generally) that if we went from C to (almost) Pascal in one go we would
loose the audience.  MISRA-C1 was so successful because it was user
friendly. A LOT of companies are using it. Their C has improved....
MISRA-C2 is a step further. Hopefully all the current MISRA users will
move to it.  MISRA-C3 will be another step forward.

You don't run a marathon by running 26 miles on day one of training.

Quoted text here. Click to load it

Whereas mine English is perrfek :-)

Quoted text here. Click to load it

OK. Though there are others involved who would argue their corner...  IT
would make a fun discussion over a bottle of scotch one night but
probably not for public consumption.


Quoted text here. Click to load it

:-)
I think he referring to C99  he has used that analogy at several ISO C
meetings. This is why  we are still working with C90 at the moment.

Quoted text here. Click to load it

Logical. I think part of the problem is that Ada is usually (always?)
taught in a high integrity context.  C is usually taught is an appalling
way.

I have had one lecturer tell me he taught C but used cin and cout in
strad of print and scanf as they were too difficult and anyway C was
simply a sub-set of C++....  (another candidate for a thread of it's own
:-)

Quoted text here. Click to load it

Yes if they must use C at least we can improve the usage.

Quoted text here. Click to load it

Fair enough.


That I can't disagree with. In fact part of my presentation at the 2002
MISRA forum was the problem that there is no MISRA-C certification of
tools anyone could interpret as they saw fit and claim what they like.
SOme claimed things there were not (in my view) supportable

Quoted text here. Click to load it
Yes.. things have been made a little difficult by some of the claims...
"we test 100% of MISRA"*

*That is we test 100% of the rules we thing our tool can test.... :-(

Quoted text here. Click to load it

Hopefully. There are a few things in the pipeline that will be announced
in Feb/March

Quoted text here. Click to load it

It will be better. How much better we will have to see but anything that
improves the general level of embedded C programming has to be a Good
Thing (tm)


Quoted text here. Click to load it

Good point.


The point was that C has been used successfully in these areas. At one
time it was said no HLL could be used in these areas.


Quoted text here. Click to load it

I was once asked to set up a Modula2 system... in theory the language
was good but I discovered that the compiler had been written in x86
assembler, there was a most of a user manual but when I contacted the
company that wrote the compiler the programmer had left and they had no
design documentation, notes or bug fixes. No evidence of any testing
etc.

In theory the language was good but the tools we had were not safe.

Quoted text here. Click to load it

Cue the Black Adder Goes Forth* sketch in what happens when you don't
pooh-pooh the pooh-pooh... (this will require a new NG not just a new
thread)

(Forth? even he had an opinion on languages)  


Quoted text here. Click to load it

Happy New Year? with you waiting to analyse every line of MISRA-C2... I
shall need tranquillisers :-)

BTW Re your Correctness by Construction: Better can also be cheaper...
Interesting reading. I also use the line "better is also cheaper" when
discussing C programming

Regards & Happy New Year

Chris


/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ 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

Rice's theorem states this.  It is a result of the undecidablility of the
Halting problem, and it is also related to Godel's incompleteness theorem.
I would suggest taking a class on computation theory, but it might suffice
to read a book on computation theory and work through the problems.

Quoted text here. Click to load it

No it isn't a contradiction.  SPARK is not a general purpose language; it is
a special purpose language (SPARK is not Turing-Complete hence Rice's
theorem doesn't apply to it), which is designed to facilitate deep static
analysis.



Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it
...

True in practice, and also in theory due to limits on memory sizes.  But
if you were to write a SPARK program that was an interpreter for a
general purpose language, verification would only result in proving that
the interpreter worked correct and say nothing about programs in the
interpreted language.

Not how you would use SPARK in any case, but it is worth remembering.
Just as I can write Ada programs that are not SPARK programs but can
statically proven to halt, or I can write an Ada program for which no
such proof is possible.  SPARK just provides a convenient way to write
programs that can be proven correct, and to automate much of the proof.

In C it is much, much harder to write programs that can be proven
correct, but it can be done.  One way is with an Ada to C translator. If
I had to produce a large safety-critical system for a chip which did not
have an Ada compiler, using an Ada to C translator (several exist) and
the SPARK tools might be a decent alternative to an Ada port.

In practice for the small programs that are common on 8-bit chips, I
find it easier to validate the generated code to the original requirements.

--
                                           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 believe SPARK is a finite language.  That is you can only declare finite
data structures.  In general purpose languages you can declare infinite data
structures, which are needed to be Turing-Complete.  Most compilers (and
computers) only support subsets of general purpose programming language ;-)

Quoted text here. Click to load it

Well if you had some nice properties about the interpreted language then the
verification of the interpreter would imply that those program apply to the
program while they are being interpreted. I know---I am nitpicking, but I
have been trained to.

Quoted text here. Click to load it

I believe the SPARK examiner is written in SPARK. ;-)

Quoted text here. Click to load it

I completely agree.  I just get excited about SPARK because it is one of the
few formal tools situated toward the end of the verify/validation chain.
For instances for a formal methods class, I used Promela and LOTOS to prove
a theorem for a safety property about a set of traffic lights for a one lane
bridge.  With SPARK I was able to able to prove that the premise of that
theorem was satisfied by the traffic controller program that I wrote.

Quoted text here. Click to load it

I agree.  However, directly working with proofs about programs written in C
would probably not be a process that you could pick up in a week to finish a
class project ;-)

Quoted text here. Click to load it

This really isn't writing C programs to be proven correct.  It is generating
them as an intermediate representation.  Once the C code is compiled, you
can still use the practice that you suggested below.

Quoted text here. Click to load it
requirements.

A wise practice considering that compilers have bugs.  However, the point of
verifying that SPARK code meets validated requirements is to detect errors
sooner to simplify the later stages of development.  Hopefully once you VV
the SPARK program, your task to VV the generated code is simplified.

-CRM
To reply by email, change the "hotmail" to "yahoo".



Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

I think we are agreeing violently. ;-)  My point is that you can use
external (from a SPARK viewpoint) storage to make SPARK Turing-Complete.
  For an example, consider an embedded system that includes a tape drive
for data logging. The system as a whole is Turing Complete, given an
operator to change tapes, but it wouldn't normally be used in that way.

So you would be able to prove that a package that used the tape drive to
implement a stack was correct, but you couldn't validate programs that
used the tape as an unbounded store.

Once you get into this situation, which I have run into on several
projects you have to decide where to make the cut.  I remember one
particular (pre-SPARK) Ada project where we validated that the program
would not fail if it ran out of logging space, and that the amount of
logging space available met the system spec.  We just had to live with
the fact that the logging requirement was somewhat arbitrary.

--
                                           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

Yep. We are agreeing.  I was going to use the tape drive example but you
beat me to it.

Quoted text here. Click to load it

Interesting...I had always suspected that this had to happen in practice,
but I didn't actually know how professionals (at least a set of
professionals;) reacted to these sorts of impasses.  Thank you, I bet this
bit of information will turn up useful to me sometime in the future.

-CRM



Re: Certified C compilers for safety-critical embedded systems



[snip]
Quoted text here. Click to load it

Funny you should mention that.  We are currently doing exactly this for
an aviation project.  Tool chain is UML to SPARK to C.  Most of the
verification activity will be done on the SPARK intermediate "design
model".  We have found that SPARK to C translation is much easier than
Ada to C translation.  For example, verification activities at the SPARK
level eliminate the requirement to add run-time checks to the C (which
is therefore very easy to compare against the SPARK source);
furthermore, the use of SPARK laregly eliminates the need for a run-time
library so all the C is directly traceable to user-written SPARK statements.

I have submitted a paper on this to Ada Europe.  We are also in the
process of productising the process (probably in the form of a "generate
C" switch for the SPARK Examiner.

regards

Peter


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

This may be just as well, since IMO part of the C problem is the
extreme reuse and terseness of tokens and the perverse precedence
rules.  

No language can be proof against errors, it can only supply extra
redundancy and increase the likelihood of detection at compile
time or detection at run time via appropriate checks.
Unfortunately the latter will always require a means of
disablement, and the psychology of programmers is such that that
will be used unnecessarily.

Quoted text here. Click to load it
... snip ...
Quoted text here. Click to load it

Again, I consider splint annotatated C to be another language,
with an even more unnatural syntax.  Also, the best people DO make
those kinds of mistakes, and I present myself as evidence.
Unfortunately many of the best programmers are somewhat sot in
their ways, and will reach for the C system as opposed to learning
an Ada or Pascal system, just as not too long ago they reached for
the assembler rather than learn Fortran, PL/I, Pascal, or C.
Availability also has a hand in here.

I consider the ideal mixture for embedded systems to be a
combination of assembly, C, and Pascal.  The result can be trimmed
down to the abilities of highly incapable hardware, and yet can be
made mutually compatible.  I think (and I am willing to be
corrected) that Ada cannot be trimmed substantially and still be
Ada, and even if it can the extra verbiage will deter users.  

--
Chuck F ( snipped-for-privacy@yahoo.com) ( snipped-for-privacy@worldnet.att.net)
   Available for consulting/temporary embedded and systems.
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 think the subset of Ada used by SPARK is a good counter-example.  It's
not the only one in use, since Ada provides pragmas that restrict
functionality to achieve a higher level of determinism, or to
reduce/remove the need for runtime library support.

- Ed

Re: Certified C compilers for safety-critical embedded systems
It is possible to write interrupt drivers so the math is the same as polled
code.

w..



tanya wrote:

Quoted text here. Click to load it


Re: Certified C compilers - and interrupt code
Quoted text here. Click to load it

That remains true, but hardly anyone today strives to "prove
mathematical" correctness. The problem is that Every Instruction
could potentially be followed by All interrupt code, unless the
interrupts were known to be disabled in a block of code.  What
the instruction set designers Ought to have invented is a subroutine
call that says turn-off-interrupts-and-call and a corresponding
return-and-restore interrupts, then code checkers would have shot.



Quoted text here. Click to load it

But the results were more deterministic, even if latencies were
worse. That is still the tradeoff, isn't it?

Quoted text here. Click to load it

Most likely.


No question.


BINGO!

Rick
Merrill


Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

SPARK is a subset of Ada.



Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

From a medical equipment point of view, the tool (being the C Compiler
in this case) has to be demonstrated to be appropriate for use and
that appropriate mitigations are in place in the event of it's
failure. The issue of whether it is "inherently unsafe" and thus
unsuitable to use,  is a developer decision. The FDA guidelines on 3rd
Party tools mandates a risk analysis be performed on the system and
thus this would lead to fault analysis of the components used. The
fault in the compiler, such as producing incorrect code, would have a
mitigation. In any case, anyone developing software for
safety-critical systems would have their own acceptance criteria for
the compiler and not soley rely on a piece of paper saying that it's
ISO C compliant or whatever.

A don't disagree that probably Ada and Pascal are better languages to
program in but their use restricts the choices of microprocessors that
can be used. Pragmatically the device that is to be developed has to
be commercially viable.  Also the experience depth of those software
engineers who know Pascal and Ada are limited.

The approach of using C or any language in a safety-critical
application is to ensure an appropriate degree of testing, commiserate
to the level of criticality, is applied to all levels of testing from
unit, integration and system. For example, for the level of
criticality, if 100% structural coverage in unit testing is desired
then this may mean that the software should be designed for
testability. This in my mind is the more important aspect, rather than
whether the compiler is C or Ada (even if Ada were "certified" safe).

Ken.

+====================================+
I hate junk email. Please direct any
genuine email to: kenlee at hotpop.com

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

Quite a lot of people use C in automotive systems. Somethings can be done
which reduce risk. The first is to use a subset of the language usually
something like the MISRA C standard. There are tools availible from several
companies which check compliance against such standards.

The other thing is to either only use minimal or no optimisation at all so
the mapping of C to machine code is as exact as possible.

Of course this only facilitates the testing that must be done it doesn't
remove the need for it.

-p
--
Paul Gotch
CoreSight Tools
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

Sorry, but MISRA is not to C what SPARK is to Ada.

MISRA is a collection of seemingly-random, often contradictory
guidelines that attempt to steer the programmer away from the darker
corners of the language.  Some of the rules are good, some bad, some
indifferent, some are impossible to break (e.g., Rule 85, "don't call
a function that takes no parameters without an empty set of
parentheses"), and some are impossible to understand (e.g., Rule 29,
"The use of a tag shall agree with its declaration").

The best thing about MISRA is that it gives you permission to break
the rules if you have to.  And you _will_ have to.  For example, rule
3 says "break rule 1".  In almost exactly those words.

Following MISRA will not (in itself) result in better code.  It will
allow you to check off a MISRA box (if your customer has one).  That's
about it.

But tools.  Now _there's_ an idea.  Specifically lint.  Especially
Gimpel's PC-lint or FlexeLint.  Lint early.  Lint often.  Lint is your
friend.  (Now where have I heard that before?  ;-)

Note it is very important to _understand_ the messages lint is giving
you, not just work around or disable them.  You will learn a lot about
C and a lot about your code and how the compiler must translate it.
If you do this, you _will_ get better code.

Regards,

                               -=Dave
--
Change is inevitable, progress is not.

Re: Certified C compilers for safety-critical embedded systems
On Thu, 18 Dec 2003 15:20:30 GMT, snipped-for-privacy@hotmail.com (Dave Hansen)

Quoted text here. Click to load it

Yes. I like lint. A valuable tool, once set up properly. However,
every user should be required to memorize your second paragraph and
recite it at least four times per day :-)

Some modern compilers do a pretty good job when set for max warnings.

--
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


If you read Safer C by Les Hatton you will discover that Ada and Pascal
are in practice no safer than C

Quoted text here. Click to load it

this is correct. At the moment only one C compiler claims to be ISO C
compliant.



/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ 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

Which one ?
--
Ignacio G.T.

Re: Certified C compilers for safety-critical embedded systems
snipped-for-privacy@evomer.yahoo.es> writes
Quoted text here. Click to load it
AFAIK The Altium/Tasking Tricore compiler
/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\
\/\/\/\/\ 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

Well, this article discusses a review, by the UK Ministry of Defense,
of code certified at DO-178B Level A.  Thus it is reasonable to
consider it an apples-vs-apples comparison.  The review found that Ada
code had only 10% of the residual errors of C code, and that SPARK
code had only 1% of the residual errors of C code.

http://www.sparkada.com/downloads/Mar2002Amey.pdf

Mike

Site Timeline