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

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

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

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

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

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

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

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

调度感知同步数据流建模

对流应用系统进行吞吐量分析需要将周期静态顺序调度建模到数据流图中,吞吐量分析效率依赖于数据流图的规模及建模时间。为了提高吞吐量分析效率,提出基于同构同步数据流图的调度感知同步数据流模型及相应建模方法。通过利用应用模型结构特征及周期静态顺序调度,可减少模型中的任务、边和初始符号数目;可以使用已有分析方法对模型进行吞吐量分析。实验结果表明,所提建模方法优于已有方法,可有效提高吞吐量分析效率。

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

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

同步数据流程序的可信排序

Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效提高编译器的安全性。因为Lustre程序是并发执行的,需要对其进行因果分析和串行化。利用Coq工具,形式化定义拓扑排序的性质和相应层次的Lustre的语义;对Lustre程序进行因果分析和排序;证明排序后的程序满足拓扑排序的性质;证明任意两个满足拓扑排序性质的程序语义执行等价。从而实现了一种针对Lustre程序的可信排序过程。

基于异构多核平台的同步数据流图帕累托优化与调度

同步数据流图被广泛用于多媒体和数字信号处理程序等流应用程序的建模。流应用程序须达到一定吞吐量才能流畅运行,利用异构多核处理器来进一步提高流应用程序的吞吐量已经成为当今嵌入式系统的发展趋势,但是提高吞吐量往往伴随着能耗的增加。为了解决这个问题,基于异构多核平台的同步数据流图系统模型,给出了求解所有能耗和吞吐量的帕累托优化点及其相应静态调度的方法。首先将系统模型转换为时间自动机网络,并将分析目标转换为时序逻辑公式;再使用实时模型检测工具UPPAAL寻找解决方案;最后对UPPAAL返回的结果进行分析,找出满足要求的调度。由于模型检测方法可对问题空间进行穷尽搜索,该方法得到的结果是精确的。该方法可帮助设计者在系统开发早期了解系统能耗和吞吐量的量化关系,有利于缩短系统的开发周期,降低开发成本。

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

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

同步数据流模型调度序列的空间优化

提出了一种嵌入式DSP系统的存储优化方法。该方法基于同步数据流模型SDF(Synchronous Data Flow)。针对其他优化算法不适用于存在反馈环的同步数据流模型的问题,该方法为反馈环的空间优化设计实现了启发式的调度算法,并提出了将SAS(Single Appearance Schedules)和Non-SAS类型调度序列相结合的层次化的空间优化方案,为同步数据流模型调度序列的空间优化提供一个通用的解决方案。实验结果证实了该方案的有效性。

基于同步多维数据流的脑网络动态特征辨识方法研究

针对人脑实时变化的特性,为了更好地观测和描述人脑网络的动态特征,在基于功能磁共振成像的脑功能网络重构技术基础上,给出了一种人脑网络动态特征辨识方法。首先利用同步多维数据流的即时更新能力,将在静息态功能磁共振成像数据采集区间上的血氧水平依赖信号由大时间序列分解重构为每个采样点上的小时间窗口序列,构建连续时间点上的状态观测窗口,从而实现对人脑功能共振信号的特定时间状态辨识;然后运用相关分析对状态观测窗口信号进行分析,得到单状态观测矩阵,最终构建全脑在整个数据采集区间上的动态特征矩阵。实验结果显示该方法可以为人脑网络的动态特征观测和描述提供一种有效手段,也为进一步研究人脑网络的动态特征演变奠定了基础。

基于钉钉的重点项目管理系统构建

针对传统项目管理方式存在的监管难和监督滞后等问题,本文研究了重点项目信息化管理平台体系架构,设计实现了基于钉钉审批流和待办事项的重点项目管理系统,实现了重点项目的移动端填报、进度管理和审批功能。系统的应用提高了重点项目管理的效率,实现项目全周期管理。

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

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

基于图分割的流应用多处理器映射算法

为了充分利用多处理器平台所提供的计算资源,需要将应用以适当的方式映射到不同处理器,从而最大程度地挖掘应用所提供的并发性以满足应用严格的实时性要求。提出了并发图来量化、建模应用任务间的并发性,提出了一种基于自同步调度的并发图构建算法,并将任务映射问题转换成图分割问题,然后将并发图分割问题建模为纯0-1整数线性规划模型并采用ILP求解器获得最优解。采用了大量随机生成的同步数据流图以及一组实际应用对所提方法进行性能评估,实验结果表明所提方法性能优于已有算法。

基于PtolemyⅡ的自主飞行器控制系统代码生成及应用

为解决自主飞行器控制系统设计中存在的复杂的代码制造问题,引入基于计算模型的设计方法,使用适合于控制系统建模的同步数据流计算模型来指导模型中各个模块之间的交互通讯,通过进行静态分析决定模块的执行顺序并能以此产生相应代码。在Ptolemy II图形语言开发环境下,以同步数据流计算模型对自主飞行器实时控制系统进行有效建模,并在此计算模型指导下自动生成代码,而所生成的代码能实施在实时分布式计算平台上,实现自主飞行器单机自主飞行的硬件在环仿真。

嵌入式DSP系统中SDF模型的层次化存储优化方法

在同步数据流模型(SDF)描述的嵌入式数字信号处理(DSP)系统中,计算体单一出现调度(SAS)算法对于存在反馈环和数据密集处理的应用不可解或内存优化效果很差.文中提出了将SAS和Non-SAS类型调度算法相结合的层次化的存储优化方法,定义了数据密集分量和强连通分量来描述环和数据密集处理结构,并依据数据优先消耗原则设计了启发式的Non-SAS调度算法对分量进行存储优化.该方法适用于任意SDF模型,并有良好的存储优化效果.实验结果证明了其有效性.

使用SDF图描述的嵌入式DSP系统存储优化

提出一种嵌入式DSP系统的存储优化方法 该方法利用遗传算法求得存储需求量较少的同步数据流 (Syn chronousDataFlow ,SDF)图顶点调度序列 ;使用TPFIFO(Two PortFIFO)数据缓冲模型来实现顶点输入边和输出边的存储共享 ,以进一步提高数据缓冲的利用率

可信编译器中地址不相交的保持性证明

同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言,在同步数据流语言到顺序执行语言的翻译转换过程中,语义等价要保证赋值语句的左右值地址互不相交,这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质,并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。

基于FBG应变传感器的隧道安全实时监测算法研究

讨论了埋入式光纤Bragg光栅应变传感器在某隧道施工期间的实际安全监测原理、布局和数据采集,在此基础上对同一截面上所采集的同步多维应变数据流进行了数据分析,给出了一种基于双重滑动窗口模型技术的异常数据实时诊断算法,该方法通过第1个滑动窗口将当前光纤Bragg光栅传感器应力数据与历史数据合并形成当前观测窗口数据,对每个观测窗口内的数据进行主成分分析,并提取其对应的特征向量,得到当前时刻的动态特征;接着采用第2个滑动窗口技术,将得到的当前时刻第一主成分特征向量与历史动态特征合并成为动态特征矩阵并展开相关性分析,最后通过计算相关系数的方差变化来判断数据的稳定性。现场的实际观测结果和对比实验结果证明该方法达到了更好的实时监测效果,同时该方法也为光纤Bragg光栅应变传感器在工程安全实时监测中的应用提供了有力支持。