可信编译器中地址不相交的保持性证明--控制网

可信编译器中地址不相交的保持性证明
企业:北京广利核系统工程有限公司 日期:2017-04-25
领域:工业安全 点击数:308

北京广利核系统工程有限公司 谷伟卿,张智慧,白涛,齐敏

摘要:同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言,在同步数据流语言到顺序执行语言的翻译转换过程中,语义等价要保证赋值语句的左右值地址互不相交,这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质,并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。

关键词:同步数据流;定理证明;Coq;语义等价;地址不相交

在线预览:可信编译器中地址不相交的保持性证明

摘自《自动化博览》2017年4月刊

  • 在线反馈
1.我有以下需求:



2.详细的需求:
姓名:
单位:
电话:
邮件: