可信编译器中地址不相交的保持性证明
|
摘要
同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言,在同步数据流语言到顺序执行语言的翻译转换过程中,语义等价要保证赋值语句的左右值地址互不相交,这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质,并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。
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.
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.
引文
[1]高玉娜.基于SCADE的嵌入式软件开发方法研究[J].电子设计工程,2015,21:103-105.
[2]何炎祥,吴伟,刘陶,等.可信编译理论及其核心实现技术:研究综述[J].计算机科学与探索,2011,05(1):1-22.
[3]Berry G.Synchronous design and verification of critical embedded systems using SCADE and Esterel[C].Formal methods for industrial critical systems,2007:2-2.
[4]Clarke E M,Wing J M.Formal methods:state of the art and future directions[J].Acm Computing Surveys,1996,28(4):626-643.
[5]韩俊刚,杜慧敏.数字硬件的形式化验证[M].北京:北京大学出版社,2001,12.
[6]Coqdevelopmentteam B.The coq proof assistant reference manual-version 8.0[C].INRIA,INRIA Rocquencourt.2010.
[7]刘洋,甘元科,王生原,等.同步数据流语言高阶运算消去的可信翻译[J].软件学报,2015,26(2):332-347.
[8]Yang X,Chen Y,Eide E,et al.Finding and understanding bugs in C compilers.[J].Acm Sigplan Notices,2015,46(6):283-294.
[9]张智慧,齐敏,冀建伟,等.核安全级控制算法描述语言的可信编译研究[C].2011.
[10]石刚,王生原,董渊,等.同步数据流语言可信编译器的构造[J].软件学报,2014,25(2):341-356.
[11]王蕾,石刚,董渊,等.一个C语言安全子集的可信编译器[J].计算机科学,2013,40(9):30-34.
[12]甘元科,张玲波,石刚,等.同步数据流程序的可信排序[J].计算机应用与软件,2014(5):1-5.
[13]张玲波,甘元科,石刚,等.同步数据流语言时态消去的可信翻译[J].计算机工程与设计,2014,35(1):137-143.
[2]何炎祥,吴伟,刘陶,等.可信编译理论及其核心实现技术:研究综述[J].计算机科学与探索,2011,05(1):1-22.
[3]Berry G.Synchronous design and verification of critical embedded systems using SCADE and Esterel[C].Formal methods for industrial critical systems,2007:2-2.
[4]Clarke E M,Wing J M.Formal methods:state of the art and future directions[J].Acm Computing Surveys,1996,28(4):626-643.
[5]韩俊刚,杜慧敏.数字硬件的形式化验证[M].北京:北京大学出版社,2001,12.
[6]Coqdevelopmentteam B.The coq proof assistant reference manual-version 8.0[C].INRIA,INRIA Rocquencourt.2010.
[7]刘洋,甘元科,王生原,等.同步数据流语言高阶运算消去的可信翻译[J].软件学报,2015,26(2):332-347.
[8]Yang X,Chen Y,Eide E,et al.Finding and understanding bugs in C compilers.[J].Acm Sigplan Notices,2015,46(6):283-294.
[9]张智慧,齐敏,冀建伟,等.核安全级控制算法描述语言的可信编译研究[C].2011.
[10]石刚,王生原,董渊,等.同步数据流语言可信编译器的构造[J].软件学报,2014,25(2):341-356.
[11]王蕾,石刚,董渊,等.一个C语言安全子集的可信编译器[J].计算机科学,2013,40(9):30-34.
[12]甘元科,张玲波,石刚,等.同步数据流程序的可信排序[J].计算机应用与软件,2014(5):1-5.
[13]张玲波,甘元科,石刚,等.同步数据流语言时态消去的可信翻译[J].计算机工程与设计,2014,35(1):137-143.