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

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

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

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

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

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

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

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

单率异步数据流语言的RTL文法设计

数据流语言是面向虚拟仪器的可视化编程环境的核心 .为了使这些基于数据流的编程环境能够应用到实时系统设计中 ,必须引入一种严格定义的实时文法 .RTL文法适合描述数据流语言 ,但是异步节点的表述问题以及时间基准选择问题并未解决 .提出了一种用于描述单率、异步数据流语言的 RTL文法 .该文法中引入传输事件常量与状态谓词 (state predicates)解决了异步节点的

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

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

数据流语言中数据频率的自动化处理技术

数据流分析和处理是计算机应用最常见的工作之一,实际系统常常包括不同频率的数据流,而现有的程序语言要求在程序中对数据频率进行显式的处理.旨在提出一种新型的变频数据流处理框架,针对基本的频率运算进行自动化处理.我们基于函数式程序设计语言和依赖类型系统理论,定义了数据流语言FStream,在程序的类型检查过程中对数据流频率进行检查和处理,并给出了离散的Simulink模型到FStream的表示.

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

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

数据流语言

本文介绍了一种新型的计算机语言──数据流语言，并讨论数据流语言的特性和它的执行模式、设计规则。

数据流可视化语言LabScene的连线设计

连线作为数据流可视化语言编辑器的重要组成部分,一方面要表示逻辑上的数据依赖关系,另一方面自身要以容易理解的物理形式展示出来。为了有机地整合这两个属性,该文提出了线树的概念,利用线树的结构表示逻辑属性,线树的节点表示物理属性,使得两个属性既相互关联又相互独立,从而为解析运行提供完整的逻辑信息且容易进行编辑和优化。该设计已在面向虚拟仪器开发的数据流可视化语言LabScene中实现。

数据流可视化语言的运行模型

提出了基于事件的异步运行模型(EADF),并给出了该模型的文法描述、调度算法以及在自主研制的面向虚拟仪器领域的DFVPL:LabScene2.0中的实现方法。以地面核磁共振找水仪的仿真系统为实例进行了分析说明。基于EADF的DFVPL减少了程序员在并行计算上的设计,对于可静态规划的循环、计算量大的运算、网络和本地I/O资源的获取上性能有显著的提高。

数据流计算

本文介绍数据流和数据流计算有关的概念,筒要分析数据流系统结构的几种实现,并对它进行评价。还将讨论一种数据流编译器和一种数据流语言。

事件触发并发数据流模型

DHDF(动态纯数据流)是许多图形化编程平台的核心.由于它的自然属性(数据驱动)与操作系统事件驱动模型不能很好地结合,导致了两个明显的不足:运行效率低,CPU占用率高;对外部事件响应速度慢,系统实时性差.提出了一种ECDF(事件触发并发数据流)模型,并给出了该模型的文法描述以及调度算法.ECDF模型通过引入多优先级线程以及事件触发机制,在很大程度上提高了系统的实时性与运行效率.以测试系统为背景,对有关应用实例进行测试与分析,结果表明,与DHDF模型相比,ECDF模型使系统的性能在不同条件下都得到了相应的提高.该模型特别适用于处理突发性高速数据流,也适用于Reactive系统设计.

基于扩展XQuery引擎的空间数据流查询方法研究

针对目前XML数据流处理中通常采用的查询语言XPath和XQuery均不支持空间运算,无法应用到空间数据流处理技术中的问题,设计了一种通过扩展现有商业化XQuery引擎功能基础上的空间数据流检索方法。

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

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

图形化编程平台运行算法的研究

主要通过可视化编程语言的研究 ,在开发面向虚拟仪器系统的图形化编程平台 (GPP)中提出了基于改进数据流语言的程序运行算法。该算法采用数据驱动的方式 ,实现了GPP元件的数据处理及元件之间的数据传递和数据类型转换等一套完善的运行机制。

语法制导生成的虚拟仪器开发平台

如何以一种与特殊的图形用户接口无关的形式一致地描述数据流可视化编程语言及其开发平台,成为虚拟仪器开发平台自动生成的主要问题。该文以自主研制的开发平台LabScene为例,形式化地描述其中最主要的3个部分:编辑,运行,调试,把这些形式化的描述翻译成C#语言,实现自动生成,为以非数据流为核心的虚拟仪器开发平台的自动生成提供参考依据。

面向虚拟仪器的DFVPL:LabScene的自动连线

针对目前大多数数据流可视化编程语言(DFVPL)不提供自动连线或者提供的自动连线对用户在连线过程中的设计意图表达不够准确的情况,提出了面向虚拟仪器领域的DFV-PL的自动连线框架。通过有机地整合连线距离、逻辑关系、类型匹配等诸多因素,并利用生成虚拟仪器软件的逻辑顺序设计了自动连线方法。此设计已在自主研制的面向虚拟仪器开发的DFVPL:LabScene中实现,并可作为其他领域的DFVPL自动连线设计的参考。

NI LabVIEW 8.20提高设计能力

美国国家仪器有限公司（NI）正式推出LabVIEW8．20版本一这是专用于控制、测试和嵌入式系统开发的LabVIEW图形化系统设计平台的20周年纪念版。LabVIEW 8．20通过自带的MathScript对基于文本的数学算法提供支持，从而扩展了LabVIEW图形化数据流语言的功能，工程师们可以集成他们现有的、在MATLAB软件中创建的m文件，或者在LabVIEW中创建新的脚本，将图形与文本语言结合在一起从而满足他们的设计应用需求，并快速完成系统原型。