Re: Certified C compilers for safety-critical embedded systems

From: Chris Hills (chris_at_phaedsys.org)
Date: 12/30/03 

Date: Tue, 30 Dec 2003 18:01:56 +0000

In article <bshl7d$1gab$1@msunews.cl.msu.edu>, Chad R. Meiners
<crmeiners@hotmail.com> writes
>
>"Chris Hills" <chris@phaedsys.org> wrote in message
>news:fUk12TA8gB7$EA$E@phaedsys.demon.co.uk...
>> 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
>
>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.

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

Quantcast