从Lustre到C语言——KCG
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
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
本博客所有文章除特别声明外,均采用 CC BY-NC-SA 4.0 许可协议。转载请注明来自 Fifish's BBlog!