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

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

面向大规模AI数据流的可靠接入研究

随着人工智能边缘化,繁杂的智能终端设备产生大规模AI数据流,这些AI数据流的实时高可靠接入对边缘接入集群提出了更高的要求。论文提出基于UDP的AI数据流通信协议和旁路控制机制,以实现数据流实时高可靠接入;提出基于AI数据单元的组确认通信机制,大大减少通信确认造成的额外开销;同时设计数据流周期同步机制以支撑GPU服务器的SPMD计算。实验结果表明,论文旁路控制机制和组确认通信可对接入网卡进行横向扩展,且在不发生AI数据包丢失情况下,论文通信方案比传统UDP通信单端口平均数据流单元并发量提升约30%。

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

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

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

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

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

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

基于实时数据同步交换技术的统一潮流控制器监控系统

研制了一种基于实时数据同步交换技术的统一潮流控制器(UPFC)监控系统,阐述了UPFC的基本工作原理,介绍了其结构、功能和通信特点。该监控系统利用双口RAM 作为共享的数据缓冲区,实现实时数据的同步交换。系统以同步并行方式工作,确保了监控的实时性。系统采用模块化设计,有很好的兼容性和扩展性。为提高可靠性,该系统还具有自检功能。

通信终端与Web服务程序数据同步设计

通过对智能终端与Web Service的研究,阐述了Web服务数据同步系统的数据接口设计和功能设计,分析了同步系统的控制流程。以手机与电话机通信终端设备数据Web同步服务为实例,给出了串行口类、短信类与号码本类设计与Web Service实现。所采用的基于SOA的Web Service封装,使Web服务数据同步系统具备自治性、多样性、可互操作性和可复用性。

面向并发程序的重构一致性检测方法

针对并发软件重构后可能带来的行为不一致问题,提出了一种重构一致性检测方法,该方法使用控制流分析和数据流分析检测重构前后的变化,使用同步依赖分析检测重构前后同步依赖关系的变化.针对对象重用性、静态共享字段、死锁3种典型的引起并发错误的情况,设计了3种检测算法对重构前后程序的不一致性进行检测.依据该方法,在WALA软件分析框架下实现了一个原型检测工具.在实验中,使用该工具在SPECjbb2005和HSQLDB测试程序上进行了验证,并与Schafer等提出的方法进行比较,实验结果表明,该方法能够有效地发现并发软件重构的不一致行为.

一种无人机红外/毫米波雷达数据融合方法

无人机用途十分广泛,不管是侦察定位,还是执行其他任务,均需要具有较高的目标跟踪定位能力,通常可将红外传感器和雷达配合使用。文章针对使用红外传感器在直角坐标系下对目标运动状态估计时不稳定且红外传感器与雷达数据率不一致的问题,提出一种将基于修正球坐标系的红外(IR)目标跟踪与毫米波雷达(mmw)跟踪结合在一起的方法,通过使用最优数据压缩方法,将红外与毫米波雷达信息融合,解决了在直角坐标系中使用红外传感器的不稳定问题以及红外传感器数据率明显高于雷达数据率的问题,实现红外与雷达同步数据融合,有效地提高无人机的目标跟踪能力。

基于扩展OAI-PMH协议的机构库流控制和数据同步研究

针对当前机构库软件存在的问题,探讨通过利用ResumptionToken参数解决机构库的流控制问题;借鉴RSS技术,为收割器提供机构库的更新信息;对OAI-PMH协议进行扩展,以增加AddFriend、Notify与PushMetadata谓词;利用通知/订阅模型解决机构库的同步问题。

SDTA:一种适合密码处理的处理器结构

提出一种基于同步数据触发结构(SDTA)的密码处理技术。利用SDTA的高并行、广谱适应和多态易用等特点,满足密码处理的高性能、强适应性和抗攻击性等要求。基于该结构的设计优化流程进行应用分析,得出瓶颈操作,通过设计相应的计算加速单元实现应用加速,且新单元可以方便地加入该结构内核中,从而减少处理器的设计时间。

机构库流控制和数据同步机制的实现

分析机构库流控制和数据同步存在的问题,利用无状态Resumption令牌实现机构库的流控制,采用Syndication和订阅/通知两种模型为机构库提供同步机制。最后利用OCLC的OAIcat收割器对机构库流控制进行测试,效果良好。

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

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

山西电网对外联络线断面潮流波动因素分析

电网联络线上潮流波动因素的分析,有助于提出合理高效的潮流控制策略,从而保证互联大电网的安全稳定运行。针对山西境内交流特高压试验示范线路长南I线投运前后,山西电网外送断面潮流波动的现象进行了分析;并通过探索性研究,提出、验证了系统频率调节效应、负荷比、旋转备用分布和联络线关口测量同步性等因素对潮流波动的影响。

FPGA和EZ_USBFX2在采集图像数据中的应用

利用FPGA和EZ_USB FX2(CY7C68013)将MT9M112(Sensor)数据准确无损地传给PC机。方案使用CY7C68013控制器工作在Slave FIFO从机方式,用Verilog HDL语言在FPGA中产生相应的控制信号,最终实现对数据的快速传输,在上位机得到Sensor采集的清晰画面。该方案的传输速度快,数据准确,可扩展到其他需要通过USB进行快速数据传输的系统。与其他采用异步通信方案相比,设计利用FPGA缓冲作用,使数据无丢失传输,最终在上位机得到的图像更加清晰流畅。该设计方案和产品达到国际先进水平。

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

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

多通道高速数据采集卡的设计

通过对多通道高速同步数据采集卡的具体设计、制作 ,对其基本功能、特点、总体设计方案。

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

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

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

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

基于FPGA的多通道出砂振动信号缓存系统研究

非侵入式出砂监测是油气开采过程中涉及到的一项关键技术。针对线性阵列式出砂监测探头的多通道同步数据缓存需求以及保证波形完整性的数据预触发需求,提出了一种适合现场可编程门阵列(Field Programmable Gate Array,FPGA)实现的,具有自适应预触发功能的多通道出砂振动信号缓存系统架构,分析了实现该系统架构的关键技术,完成了具体的逻辑设计。这种系统架构采用新的自适应预触发方法,并利用乒乓操作原理,具有良好的通道扩展性。最后,以五通道自适应预触发数据缓存系统为例,对该多通道出砂振动信号缓存系统的功能完整性进行了功能仿真和板级测试。测试结果表明,基于该架构设计的多通道数据缓存系统能够完成连续数据流的自适应预触发缓存,系统架构功能完整有效。