[SystemSafety] Critical systems Linux

[Olwen Morgan]

On 21/11/2018 14:14, Tom Ferrell wrote:
<snip>
> This qualification is based on the fact that KCG is built on a formal 
> language, LUSTRE. The proofs accomplished to demonstrate the model to 
> code conversion have been looked at repeatedly and found to be 
> complete and correct in all cases that I am aware of.

<snip>

Forgot to say this before:

There is, of course, a massive problem with the proof, namely that the 
target language C does not have formal semantics. Therefore, even if 
there are explicit formal semantics for models, there is no formal basis 
on which generated C can, strictly speaking, be proven to give correct 
implementations of them. OK, you can get round this, as the proof 
unavoidably must, by using assumed semantics, explicit or otherwise. 
Then, however, you are left with the problem of what happens if your 
compiler does not handle C in the way that the assumed semantics say it 
does. Already on this list, I have posted small C programs that 
demonstrate the awkward problem that, with only a few exceptions, C does 
not prescribe an order of evaluation for the operands of operators and 
that they can differ for the same compiler in two different source code 
contexts in the same program.

One approach to this issue is to use an ultra-strict language subset and 
proven compiler, such as the CompCert C compiler - but even that still 
leaves room for problems as regards traceability to the language 
standard. To be utterly pedantic, you cannot yet avoid having faith in 
your compiler that cannot fully be justified.

Incidentally, you're in the same boat with other languages whose 
compilers are implemented by translating their source code to C. AFAI 
recall, the Ada compiler in the GNAT tool set falls into this category.

Olwen



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181122/93866bee/attachment-0001.html>