From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: f849b,b8d52151b7b306d2 X-Google-Attributes: gidf849b,public X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-12-29 03:39:17 PST Path: archiver1.google.com!news2.google.com!fu-berlin.de!uni-berlin.de!62.164.179.118!not-for-mail From: Peter Amey Newsgroups: comp.arch.embedded,comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems Date: Mon, 29 Dec 2003 11:39:13 +0000 Message-ID: References: <3fe00b82.90228601@News.CIS.DFN.DE> <3FE026A8.3CD6A3A@yahoo.com> <3bf1uvg2ntadvahfud2rg6ujk24sora6gr@4ax.com> <2u3auvogde8ktotlaq0ldiaska3g416gus@4ax.com> <20619edc.0312221020.3fd1b4ee@posting.google.com> <20619edc.0312222106.3b369547@posting.google.com> <45cs9hAbLc6$EAAx@phaedsys.demon.co.uk> NNTP-Posting-Host: 62.164.179.118 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: news.uni-berlin.de 1072697956 15853627 62.164.179.118 ([69815]) User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.4) Gecko/20030624 Netscape/7.1 (ax) X-Accept-Language: en-us, en In-Reply-To: Xref: archiver1.google.com comp.arch.embedded:6281 comp.lang.ada:3921 Date: 2003-12-29T11:39:13+00:00 List-Id: 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