论文部分内容阅读
同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用．然而，此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一．借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的，有望最大限度地解决误编译问题．基于这种方法，开展了从同步数据流语言（Lustre为原型）到串行命令式语言（C为原型）的可信编译器构造的关键技术研究．其挑战性在于两类语言之间的巨大差异，源语言具有时钟同步，数据流、并发及流数据对象等特征，而目标语言则具有顺序控制流特征．同类研究中，目前尚无针对核心翻译过程的