Re: Certified C compilers for safety-critical embedded systems

[Chris Hills <chris@phaedsys.org>]

In article <bsmagl$e5ajv$1@ID-69815.news.uni-berlin.de>, Peter Amey
<peter.amey@praxis-cs.co.uk> writes
>
>I would much rather concentrate on technical issues here 
OK

>(for example, 
>why deep static analysis of _any_ general-purpose langauge is 
>impossible; 

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

>or, why systems of integrities in the better-than 10e-6 
>failures per hour class _require_ deep static analysis); 

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

>> Praxis has a vested interest in not letting C be used for SIL 4
>
>Praxis has a long-held commitment to using the best technology available 
>and to advancing the state of the software industry as a whole. 
That's got to be from the marketing dept :-)


> Our 
>objection to using C for SIL 4 is that it is unsuited to that task.
On its own I would agree. 

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

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?

>> AFAIK Praxis are not "involved" with MISRA-C they may have been some
>> years ago in the original version but much work has been done since
>> then. AFAIK they have not taken much, if any part, in this.
>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
The original committee stopped along while ago. 

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

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


>> AFAIK they did not make their SPADE C results available to the MISRA-C
>> working group who for the last 3 years have been working on MISRA-C2.
>
>Wrong.  We did. 

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

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

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.

>> Praxis don't have a unique view of MISRA-C.  They are one of many who
>> were involved in MISRA-C1. They are not one of the main companies who
>> were promoting and working with it in the last 5 years.
>
>The slide clearly states that this is Rod's personal view and he (with 
>appalling semantics)

Whereas mine English is perrfek :-) 

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

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.


>> Slide 6 is interesting. The quotes are out of context and misleading.
>> The Praxis presentation is clearly written with a (commercial) axe to
>> grind. I was at the MISRA-C 2002 forum. In fact I did one of the
>> presentations that has been misquoted.... 
>
>Perhaps you can recall the context in which Less Hatton's shack/swamp 
>comment can be interpreted in a positive way?

:-) 
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. 

>> As it goes on they rubbish C and surprise surprise come up with a
>> solution that is their tools.... :-) 
>
>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!

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

>> The Ada (tools) community must be rattled if it needs to spend time
>> trying to rubbish MISRA-C. Perhaps it is just sour grapes as they no
>> longer push a MISRA-C tool? 
>
>Again we are not trying to rubbish MISRA-C.  We continue to believe that 
> it is useful enterprise.

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

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

Fair enough. 

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

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

>We preferred, in that 
>situation, to say nothing rather than make claims that could not be 
>defended by logic and by reasoned argument.  
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.... :-(

>I hope that MISRA-C2 will 
>be  better; 

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

>however, my long experience of designing unambiguous and 
>analyseable programming languages leads me to believe that it won't.

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) 


>> Yet  C is used in some of the highest integrity systems around. Other
>> languages that are recommended hardly exist and certainly not on many
>> platforms.
>> 
>> Empirical evidence and a glance at 61508 may require a change in the
>> table D2.... BTW table D2 in the lecturers notes is NOT in 61598.
>> 
>> In CEI/IEC 61508:1998 Part 7 Table C1 (page 79), yes I do have my own
>> copy of 61508, all 7 parts. We find a similar table to "D2" above:
>> 
>>             Sil1   Sil2   Sil3 Sil4
>> Ada          HR    HR      R    R
>> ADA (subset) HR    HR      HR   HR
>> C            R     -      NR    NR
>> 
>> as expected  BUT
>> 
>> C (subset, codinng standard and static analysis) 
>>              HR   HR      HR     HR
>> 
>> 
>> So whilst straight ADA *is* better than vanilla C. No one would debate
>> that!  Spark ADA is no better than C with a subset, coding standard and
>> using static analysis....  IE much the same constraints as SPARK ADA has
>> over ADA...
>
>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.

Good point. 

>> I know of projects using C in Railway, space, aero and medical projects.
>Use, even widespread use, does not imply suitability.

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. 


>> PASCAL and Mod2 are mentioned but you will be hard pressed to find tool
>> for these for many targets. BTW is there ADA for the PIC, AVR and 8015?
>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.

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.

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

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)   


>have a Happy New Year
>Peter

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    /\/\/\/\/\
/\/\/ chris@phaedsys.org       www.phaedsys.org \/\/
\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/