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

Proof of the Preservation Property of Address Disjointness in Trustworthy Complier

作　　者：谷伟卿[1] 张智慧[1] 白涛[1] 齐敏[1] 

机构地区：[1]北京广利核系统工程有限公司

出　　处：《自动化博览》2017年第4期72-78,共7页Automation Panorama1

摘　　要：同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言,在同步数据流语言到顺序执行语言的翻译转换过程中,语义等价要保证赋值语句的左右值地址互不相交,这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质,并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。Synchronous data-flow language is widely used in safety critical control system such as nuclear power systems. In the process of translation from synchronous data-flow language to order execution language, it is essential to guarantee the address disjointness between left and right values in assignment statement in semantic equivalence. In this paper, we formalized the property of address disjointness during the translation process, and verified the property via theorem proving. Compiler based on this method has been applied in safety protection system at some nuclear power plant.

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

分 类 号：TP314[自动化与计算机技术—计算机软件与理论]