KCG

同步数据流语言,如 Lustre和 Signal,近年来在实时嵌入式安全攸关系统开发中得到了广泛应用,此类语言相关开发工具本身的安全性在这些领域中的准入标准也越来越严格。

例如,以 Lustre 为基础定义建模语言的 Scade工具已渗透到我国航空、航天、轨道交通及核电等安全关键领域。其代码生成器 KCG 将一种基于Lustre的建模语言翻译到C语言,或许是获得民用航空软件生产许可的第 1 个商用编译器(在我国航空、高铁及核电等领域也有广泛使用),其设计开发过程(严格的 V&V 过程)符合民航电子系统的国际标准 DO-178B,并成功应用于空客(Airbus)A340 和 A380 的设计中。

然而,DO-178B/C主要是以过程质量控制为主的标准,不足以说明Scade的编译器不存在“误编译”。KCG并没有通过形式化的方法加以严格验证,虽然DO-178C中包含了一些非强制的形式化相关条款,但经调研,业界的用户仍会不时发现ScadeKCG的某些翻译漏洞。

KCG Code Generator

image-20210801212923968

Operation

参考:

[1] C:\Users\huiyu\Desktop\论文\SCADE\相关文档\SCADE Suite\Training-TG-01_Day3__Lessons_127P.pdf\p90

[2] C:\Users\huiyu\Desktop\论文\SCADE\相关文档\SCADE Suite\Training-TG-01_Day4__Lessons_103P.pdf\p90