[SystemSafety] Critical systems Linux

[Peter Bernard Ladkin]

On 2018-11-22 11:47 , Olwen Morgan wrote:
> 
> On 21/11/2018 14:14, Tom Ferrell wrote:
> ...
>> 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.
> .....
> 
> There is, of course, a massive problem with the proof, namely that the target language C does not
> have formal semantics. 
I wouldn't categorise this as a "massive problem". It is an issue that is and was well-recognised.

The question is rather more direct than whether any given PL has a "formal semantics". Put bluntly:
for any code X which your code-generator generates; does X have an unambiguous behavioural semantics?

The answer from people familiar with the SCADE subset told me a while ago that yes, it looks as if
it does. There are lots of ifs and buts involved with this, of course.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181122/d284e4e1/attachment.sig>