期刊导航
期刊开放获取
唐山市科学技术情报研究..
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
4
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式：
文摘
详细
列表
相关度排序
被引量排序
时效性排序
同步数据流语言可信编译器的构造
被引量：
18
1
作者
石刚
王生原
+6 位作者
董渊
嵇智源
甘元科
张玲波
张煜承
王蕾
杨斐
《软件学报》
EI
CSCD
北大核心
2014年第2期341-356,共16页
同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解...
同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.
展开更多
关键词
同步数据流语言
经过验证的编译器
形式化
验证
形式语义
定理证明
在线阅读
下载PDF
职称材料
可信编译器L2C的核心翻译步骤及其设计与实现
被引量：
13
2
作者
尚书
甘元科
+2 位作者
石刚
王生原
董渊
《软件学报》
EI
CSCD
北大核心
2017年第5期1233-1246,共14页
同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现...
同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.
展开更多
关键词
经过验证的编译器
同步数据流语言
L2C
Coq证明辅助器
核心翻译步骤
在线阅读
下载PDF
职称材料
一个C语言安全子集的可信编译器
被引量：
3
3
作者
王蕾
石刚
+2 位作者
董渊
白晓颖
王生原
《计算机科学》
CSCD
北大核心
2013年第9期30-34,共5页
以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全...
以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估。之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率。
展开更多
关键词
可信计算
CompCert
C安全子集
经过验证的编译器
在线阅读
下载PDF
职称材料
同步数据流语言可信编译器的研究进展
被引量：
5
4
作者
杨萍
王生原
《计算机科学》
CSCD
北大核心
2019年第5期21-28,共8页
同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。...
同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等。近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决"误编译"问题,因而成为新的研究热点。文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析。
展开更多
关键词
同步数据流语言
经过验证的编译器
翻译确认
LUSTRE
SIGNAL
在线阅读
下载PDF
职称材料
题名
同步数据流语言可信编译器的构造
被引量：
18
1
作者
石刚
王生原
董渊
嵇智源
甘元科
张玲波
张煜承
王蕾
杨斐
机构
清华大学计算机科学与技术系
新疆大学信息科学与工程学院
科技部高技术研究发展中心
出处
《软件学报》
EI
CSCD
北大核心
2014年第2期341-356,共16页
基金
国家自然科学基金(61170051
61272086
90818019)
文摘
同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.
关键词
同步数据流语言
经过验证的编译器
形式化
验证
形式语义
定理证明
Keywords
synchronous data-flow language
verified compiler
formal verification
formal semantics
theorem proving
分类号
TP314 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
可信编译器L2C的核心翻译步骤及其设计与实现
被引量：
13
2
作者
尚书
甘元科
石刚
王生原
董渊
机构
清华大学计算机科学与技术系
出处
《软件学报》
EI
CSCD
北大核心
2017年第5期1233-1246,共14页
基金
国家自然科学基金(90818019
61462086)
+2 种基金
国家科技重大专项(MJ-2015-D-066)
Sino-European Laboratory of Informatics
Automation and Applied Mathematics资助项目~~
文摘
同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.
关键词
经过验证的编译器
同步数据流语言
L2C
Coq证明辅助器
核心翻译步骤
Keywords
certified compiler
synchronous data-flow language
L2C
Coq proof assistant
key translation
分类号
TP314 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
一个C语言安全子集的可信编译器
被引量：
3
3
作者
王蕾
石刚
董渊
白晓颖
王生原
机构
清华大学计算机科学与技术系
出处
《计算机科学》
CSCD
北大核心
2013年第9期30-34,共5页
基金
国家自然科学基金(61170051
61272086
+3 种基金
90818019)
国家核高基项目(2012ZX01039-004-08-02)
清华大学基础研究基金(2010Z05097)
铁道部-清华大学科技研究基金(J2010Z064)资助
文摘
以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估。之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率。
关键词
可信计算
CompCert
C安全子集
经过验证的编译器
Keywords
Trustworthy computing, CompCert, Safe subset of C language, Verified compilers
分类号
TP314 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
同步数据流语言可信编译器的研究进展
被引量：
5
4
作者
杨萍
王生原
机构
北京语言大学信息科学学院
清华大学计算机科学与技术系
出处
《计算机科学》
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 [自动化与计算机技术—计算机软件与理论]
在线阅读
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
同步数据流语言可信编译器的构造
石刚
王生原
董渊
嵇智源
甘元科
张玲波
张煜承
王蕾
杨斐
《软件学报》
EI
CSCD
北大核心
2014
18
在线阅读
下载PDF
职称材料
2
可信编译器L2C的核心翻译步骤及其设计与实现
尚书
甘元科
石刚
王生原
董渊
《软件学报》
EI
CSCD
北大核心
2017
13
在线阅读
下载PDF
职称材料
3
一个C语言安全子集的可信编译器
王蕾
石刚
董渊
白晓颖
王生原
《计算机科学》
CSCD
北大核心
2013
3
在线阅读
下载PDF
职称材料
4
同步数据流语言可信编译器的研究进展
杨萍
王生原
《计算机科学》
CSCD
北大核心
2019
5
在线阅读
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部
