Re: Certified C compilers for safety-critical embedded systems

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Robert I. Eachus wrote:

[snip]
> 
> 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.
> 

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