-
题名可信编译器构造的翻译确认方法简述
被引量：2
- 1
-
-
作者
刘洋
杨斐
石刚
闫鑫
王生原
董渊
-
机构
清华大学计算机科学与技术系
新疆大学信息科学与工程学院
太原理工大学计算机学院
-
出处
《计算机科学》
CSCD
北大核心
2014年第S1期334-338,共5页
-
基金
国家自然基金项目(61170051
612702086
90818019)资助
-
文摘
编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可信编译器的构造中。一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生。然而,这种方法可能"冻结"编译器的设计,阻碍编译器未来可能的优化和完善。翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果。介绍了翻译确认方法的概念及研究进展。
-
关键词
可信编译器
形式化验证方法
翻译确认
确认器
-
Keywords
Trusted compiler,Formal verification method,Translation validation,Validator
-
分类号
TP314
[自动化与计算机技术—计算机软件与理论]
-
-
题名翻译确认方法在核安全级GCG中的应用研究
被引量：2
- 2
-
-
作者
闫鑫
张智慧
任保华
齐敏
-
机构
北京广利核系统工程有限公司
-
出处
《自动化博览》
2018年第4期71-75,共5页
-
文摘
在核安全级数字化仪控系统中,人机交互安全控制显示装置的显示内容和控制逻辑由图形化组态工具实现。由于显示内容规模庞大,结构复杂,如何保证实现从图形到C转换的图形代码生成器(GCG)的正确性是一个难题,通过引入形式化验证方法对GCG生成过程的正确性进行验证。本文在对两种形式化验证技术比较并结合应用场景分析之后,选取了翻译确认方法,并通过示例说明了方法的可行性,为之后图形代码生成器的形式化验证工作奠定了基础。
-
关键词
图形代码生成器
形式化验证方法
翻译确认
求值流图
-
Keywords
Graphic code generator
Formal verification method
Translation validation
Value flow graph
-
分类号
TM623
[电气工程—电力系统及自动化]
TP314
[自动化与计算机技术—计算机软件与理论]
-
-
题名同步数据流语言可信编译器的研究进展
被引量：5
- 3
-
-
作者
杨萍
王生原
-
机构
北京语言大学信息科学学院
清华大学计算机科学与技术系
-
出处
《计算机科学》
CSCD
北大核心
2019年第5期21-28,共8页
-
基金
国家民用飞机重大专项项目基金(MJ-2015-D-066)
核高基重大专项(2017ZX01030-301-003)资助
-
文摘
同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等。近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决"误编译"问题,因而成为新的研究热点。文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析。
-
关键词
同步数据流语言
经过验证的编译器
翻译确认
LUSTRE
SIGNAL
-
Keywords
Synchronous data-flow languages
Certified compilers
Translation validation
Lustre
Signal
-
分类号
TP314
[自动化与计算机技术—计算机软件与理论]
-
