检索结果-内蒙古大学图书馆

西华大学学报(自然科学版) 2025年第2期44卷 87-95页

作者：李春燕赵长名杨斐马权侯荣彬成都信息工程大学计算机学院四川成都610225 中国核动力研究设计院核反应堆系统设计技术重点实验室四川成都610041

文章对同步数据流语言的pre算子进行详细处理,除了将pre算子翻译至fby算子,还对pre算子在第一周期的值根据其输入参数类型的不同做了相应的初始化,解决了pre算子第一周期为空的问题。输入参数为整型和布尔型,其第一周期初始化为false,... 详细信息

文章对同步数据流语言的pre算子进行详细处理,除了将pre算子翻译至fby算子,还对pre算子在第一周期的值根据其输入参数类型的不同做了相应的初始化,解决了pre算子第一周期为空的问题。输入参数为整型和布尔型,其第一周期初始化为false,浮点型初始化为浮点零;数组和结构体类型,根据其元素类型分别进行不同的初始化。由于pre算子的翻译应用场景大多在核电安全级数字化控制系统(SDCS),因此为了确保其编译的正确性及安全性,整个翻译过程在辅助定理证明器Coq完成了形式化验证。同时该翻译及验证方法在SDCS中进行试用,达到了预期的翻译效果。

关键词：同步数据流语言可信编译器形式化验证

来源：评论

学校读者我要写书评

暂无评论

同步数据流语言高阶运算消去的可信翻译

引用

软件学报 2015年第2期26卷 332-347页

作者：刘洋甘元科王生原董渊杨斐石刚闫鑫清华大学计算机科学与技术系北京100084 新疆大学信息科学与工程学院新疆乌鲁木齐830046 太原理工大学计算机学院山西太原030021

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lu... 详细信息

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.

关键词：同步数据流语言形式化验证高阶运算定理证明

来源：评论

学校读者我要写书评

暂无评论

同步数据流语言可信编译器Vélus与L2C的比较

引用

软件学报 2019年第7期30卷 2003-2017页

作者：康跃馨甘元科王生原清华大学计算机科学与技术系

同步数据流语言(如Lustre、Signal)在航空、高铁、核电等安全关键领域得到广泛应用。例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言。这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关... 详细信息

同步数据流语言(如Lustre、Signal)在航空、高铁、核电等安全关键领域得到广泛应用。例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言。这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关注。近年来,基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一,也取得了瞩目的成果,如CompCert项目实现了产品级的可信C编译器。同样,人们也采用这种方法开展了同步数据流语言可信编译器的研发工作。主要关注从事这一工作的两个长线项目,二者均研发面向基于Lustre的同步数据流语言编译器,分别以Vélus和L2C代称。对Vélus和L2C从多个重要的角度进行较为深入的分析与比较。

关键词：同步数据流语言形式化验证的编译器 Lustre语言

来源：评论

学校读者我要写书评

暂无评论

同步数据流语言可信编译器的构造

引用

软件学报 2014年第2期25卷 341-356页

作者：石刚王生原董渊嵇智源甘元科张玲波张煜承王蕾杨斐清华大学计算机科学与技术系北京100084 新疆大学信息科学与工程学院新疆乌鲁木齐830046 科技部高技术研究发展中心北京100044

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解... 详细信息

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.

关键词：同步数据流语言经过验证的编译器形式化验证形式语义定理证明

来源：评论

学校读者我要写书评

暂无评论

同步数据流语言可信编译器的研究进展

引用

计算机科学 2019年第5期46卷 21-28页

作者：杨萍王生原北京语言大学信息科学学院北京100083 清华大学计算机科学与技术系北京100084

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。... 详细信息

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等。近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决"误编译"问题,因而成为新的研究热点。文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析。

关键词：同步数据流语言经过验证的编译器翻译确认 Lustre Signal

来源：评论

学校读者我要写书评

暂无评论

同步数据流语言时态消去的可信翻译

引用

计算机工程与设计 2014年第1期35卷 137-143页

作者：张玲波甘元科石刚王生原董渊张智慧王沿海清华大学计算机科学与技术系北京100084 北京广利核系统工程有限公司北京100094

为解决实现同步数据流语言Lustre到串行命令式语言C语言可信编译器过程中碰到的时态运算翻译的困难,提出了将所有的时态运算翻译单独分层定义和证明的方法。在同步数据流语言的时态特性和C语言的循环特性分析的基础上,结合可信编译器实... 详细信息

为解决实现同步数据流语言Lustre到串行命令式语言C语言可信编译器过程中碰到的时态运算翻译的困难,提出了将所有的时态运算翻译单独分层定义和证明的方法。在同步数据流语言的时态特性和C语言的循环特性分析的基础上,结合可信编译器实现框架上下层的语言结构,使用Coq证明工具,形式化的定义了两种中间语言的语法和语义,经过分析时态翻译过程特点,归纳定义了时态变量传递性质,实现了翻译工作严格的形式化验证,最终完成了时态消去翻译的等价性证明。

关键词：同步数据流语言可信编译器形式化验证时态消去 Coq

来源：评论

学校读者我要写书评

暂无评论

同步数据流语言输入结构体的可信翻译

引用

计算机系统应用 2023年第6期32卷 269-277页

作者：刘莛杨吴锡杨斐侯荣彬马权王汝桥梁根华成都信息工程大学计算机学院成都610225 中国核动力研究设计院核反应堆系统设计技术重点实验室成都610213

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉... 详细信息

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.

关键词：同步数据流语言形式化验证仪控系统可信编译器

来源：评论

学校读者我要写书评

暂无评论

一种同步数据流编程语言——LUSTRE

引用

抗恶劣环境计算机 1996年第3期10卷 17-26页

作者：郑链

来源：评论

学校读者我要写书评

暂无评论

可信编译器L2C的核心翻译步骤及其设计与实现

引用

软件学报 2017年第5期28卷 1233-1246页

作者：尚书甘元科石刚王生原董渊清华大学计算机科学与技术系北京100084

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现... 详细信息

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.

关键词：经过验证的编译器同步数据流语言 L2C Coq证明辅助器核心翻译步骤

来源：评论

学校读者我要写书评

暂无评论

Lustre-的形式化操作语义及其性质研究

Lustre-的形式化操作语义及其性质研究

引用

作者：张力北京大学

学位级别：硕士

如今,形式化方法越来越多地被应用到与生命财产安全密切相关的计算机软件领域。其中,编程语言的形式化操作语义起着一个重要的作用,比起通常用自然语言描述的编程语言规范,形式化操作语义以数学的规范提供了一种更精确的描述方式。　　L... 详细信息

如今,形式化方法越来越多地被应用到与生命财产安全密切相关的计算机软件领域。其中,编程语言的形式化操作语义起着一个重要的作用,比起通常用自然语言描述的编程语言规范,形式化操作语义以数学的规范提供了一种更精确的描述方式。　　Lustre是一种并发的同步数据流语言,主要应用于嵌入式系统的软件开发。我们将形式化方法应用于Lustre到Clight的编译过程,Lustre-是由Lustre到Clight可信编译的一种中间语言,它是由Lustre语言的一个核心子集经过等式拓扑排序、对表达式列表的赋值进行拆分、等式化简、时态运算转化等变化后得到的顺序语言,它包括流、时钟、时态运算、node等核心概念。Lustre经过多步中间语言的转换翻译到Clight,并且通过定义每一步中间语言的形式语义,最终证明每一步翻译的语义保持性。其中,每一种中间语言的形式语义定义,直接关系到语义保持性的证明。　　本文主要研究Lustre-的形式化操作语义定义及其性质,以严格的数学规范定义了Lustre-的执行环境、格局和语义规则,讨论并证明了语义的确定性,并对于给定的程序,定义了由该程序确定的一个更为精确的格局集合,并在此基础上讨论并证明了语义的终止性。

关键词： Lustre 同步数据流语言操作语义形式化方法嵌入式系统

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：