基于SCADE的形式化验证技术的改进研究

为保证SCADE软件开发的安全性,研究了SCADE形式化验证技术,指出其不足,提出了基于代码生成器的解决方法.该方法对安全特性属性引入了逻辑描述,并利用SCADE编辑器及代码生成器的特点,对SCADE形式化验证技术进行改进,降低了模型正确性确认时人为的主观性.通过实例阐述了应用该方法进行形式化验证的一般步骤,表明了该方法是有效可行的.     

基于STP方法的SCADE模型形式化验证框架

高安全性应用开发环境(SCADE)的形式化验证组件Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质,但不能充分描述拥有复杂时序性质的安全需求。为解决该问题,构建一种SCADE状态机的时序性质验证框架,将SCADE模型转换成NuSMV模型,并将线性时态逻辑和计算树逻辑引入SCADE模型的需求规范中。分析结果表明,借助NuSMV模型检查器及其验证结果可检验复杂时序相关的安全性质,减少模型设计阶段的错误,提高系统的安全性和可靠性。     

SCADE平台下C代码的自动生成

随着航空电子软件的迅速发展,传统的软件设计方法已不能满足其效率和安全性需求.为解决传统设计方法的不足,寻求一种更有效的控制软件设计方法,高安全应用开发环境SCADE应运而生.主要介绍了高安全应用开发环境SCADE的开发背景及开发特点,并以飞机飞行控制律为例,按照SCADE软件的程序设计流程,即通过直观的图形化建模建立无人机飞行控制律模型,通过模拟仿真保证设计的正确性,最终自动生成可直接面向工程的嵌入式C代码.实验结果表明,SCADE在很大程度上实现了软件开发的自动化,节约了开发成本和开发时间,体现了SCADE环境下进行软件开发的优越性.     

一种新型的磁浮列车测速定位系统模型设计

现有磁浮列车测速定位系统所采用的技术比较单一,测速定位系统的可靠性不足,不能更好地满足各种运行环境的要求。通过分析现有磁浮列车测速定位技术的优缺点,提出了一种新型测速定位系统模型,系统模型以传感器定位技术、多普勒雷达定位技术、查询应答器定位技术为基础,通过组合逻辑对系统数据进行优化。系统模型较现有技术具有高精度、高可靠性、易工程化等优点,同时采用安全性软件开发工具SCADE对系统模型进行建模及形式化验证,验证结果表明系统模型满足设计要求。     

基于嵌入式多信息融合的列车测速定位系统

列车的测速定位是提高列车运行安全及运输效率的关键技术。为此,根据国内外研究发展现状,提出一种基于嵌入式多传感器信息融合的列车测速定位系统。通过轮轴速度传感器、多普勒雷达速度传感器、加速度计和查询应答器采集列车的状态信息,并在嵌入式系统中利用联邦Kalman滤波及融合技术对信息进行处理,实现测速轮径的自适应校正以及空转／滑行的检测与补偿,减小由于车轮磨损、空转、滑行、环境等因素造成的列车测速定位误差。Matlab仿真结果表明,该系统能够有效提高列车测速定位的精度。     

新型列车测速系统的研究与设计

本文介绍了一种基于单片机技术和光电传感器技术开发的新型列车测速系统,它区别于传统的通过测量转速和利用GPS测算列车速度的方法。本系统通过测量列车行驶在轨道上单位时间内通过的枕木个数来计算列车的运行速度。     

基于QNX的操作监控平台的设计与实现

根据QNX的Photon微图形用户接口(microGUI)的运行机理，采用自定义事件、伪终端和telnet技术、动态分配内存等方法，解决了EAST极向场电源控制系统实时网络通信、启动和终止远程进程、动态绘制波形等关键问题，实现了一个友好、高效的操作监控平台，为EAST极向场电源的稳定运行提供了有力保障。     

基于MDA与UML扩展的安全软件开发方法

为提高软件安全性,提出一种基于模型驱动架构(MDA)与统一建模语言(UML)扩展机制的安全软件开发方法。采用UML扩展机制建立系统安全相关的平台无关模型,将软件的安全性分析提前到设计的早期;利用MDA方法进行软件安全属性的建模,降低后期开发的风险与成本。图书管理系统实例验证了该方法的有效性。     

基于场景分析的系统形式化模型生成方法

采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。     

基于车牌字符边界定位的视频测速

针对卡口环境下视频测速误差大的问题,提出一种提高测速精度的方法。采用以车牌第2个字符作为车辆定位的特征块,利用小波变换分解字符的外部边界特征曲线,在低分辨率下实现目标字符的模板匹配,并获取该曲线相对模板的偏移量,在原分辨率上进行边界坐标的精细调整,完成车辆特征块的精确定位。结合字符高度固定的先验知识,确定车辆特征块所处的实际坐标系,以提高对车辆行驶距离的计算。在实际环境下,对该方法进行长达2个多小时的测试,并对测试结果与线圈测速、基于车牌定位的视频测速进行对比,结果表明,在车辆正常行驶的速度下,与线圈测速相比,该方法视频测速误差在3 km/h以内。     

基于代数的软件过程建模系统的设计与实现

软件过程建模的主要目的是建立组织内软件开发过程的模型,使得软件开发过程在整个组织内获得一致的理解,进而提高软件开发效率和改进软件生产质量.软件过程建模语言一方面要易于理解、具有较强的表达能力,同时也要易于分析和验证,以保证所要描述的软件过程的正确性.介绍了基于代数的软件过程建模系统ASPMS的设计和实现,该系统提供了图形化的建模表示方式,而该图形化表示方式具有基于多元π演算的形式化语义,从而较好地平衡了建模语言的易于理解、具有较强的表达能力和易于分析和验证这一矛盾的内在要求.     

SCADE平台下的图形化设计和代码自动生成

随着航空机载软件功能和复杂性的提高,采用传统的人工编码方法来已不能满足其效率和安全性要求,因此寻求一种更有效的航空机载软件设计方法势在必行。本文研究了一种航空机载软件开发方法—高安全性开发环境SCADE,并以飞机自主导航软件为例,按照SCADE软件的程序设计流程,即通过直观的图形化建模和模拟仿真自动生成可直接面向工程的安全嵌入式C代码。实验结果表明,SCADE在很大程度上实现了软件开发的自动化,节约了开发成本和开发时间。     

基于光纤干涉定位系统的信号解调技术

基于光纤干涉的定位系统是一种新型的位置传感器系统,可用于长距离通信干线的定位监测。以往的文献对此系统的输出信号直接作快速傅里叶变换,对外界微扰动信号进行定位。在讨论了系统结构及原理的基础上,提出了一种相位解调算法,用以解决系统对大扰动信号的定位问题,并用软件实现了信号的解调。解调的结果如实地反映了原始扰动信号,保证了定位的精确性。     

Bounded model checking of C++ programs based on the Qt cross‐platform framework

The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, technology companies tend to invest in fast and automatic verification mechanisms, to create robust systems and reduce product recall rates. In addition, further development‐time reduction and system robustness can be achieved through cross‐platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present paper proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), known as the Efficient SMT‐based Context‐Bounded Model Checker, for verifying actual Qt‐based applications, with a success rate of 89%, for the developed benchmark suite. Furthermore, the simplified version of the Qt framework, named as Qt Operational Model, was also evaluated using other state‐of‐the‐art verifiers for C++ programs. In fact, Qt Operational Model was combined with 2 different verification approaches: explicit‐state model checking and also symbolic (bounded) model checking, during the experimental evaluation, which highlights its flexibility. The proposed methodology is the first one to formally verify Qt‐based applications, which has the potential to devise new directions for software verification of portable code.     

基于软硬件协同形式验证的固件漏洞分析技术

为了系统高效地分析固件中潜在的安全隐患,提出了一种基于行为时序逻辑 TLA 的软硬件协同形式验证方法。通过对固件工作过程中的软硬件交互机制进行形式建模分析,在动态调整攻击模型的基础上,发现了固件更新过程中存在的安全漏洞,并通过实验证实了该漏洞的存在,从而证明了形式验证方法的可靠性。     

基于SCADE的无人机三余度飞控系统设计及实现

利用一种嵌入式软件开发的新方法--嵌入式代码自动生成软件SACDE研究了无人机三余度飞控系统的开发.通过与传统三余度飞控系统开发方法进行了对比,说明了使用SCADE开发的无人机三余度飞控系统具有成本低、周期短、安全性高、交互界面友好等优点,并在很大程度上实现了该软件开发的自动化.     

嵌入式测姿系统软件的模块化

由于嵌入式测姿系统软件根据不用需求需实现多种接收机板卡、不同导航系统、多种姿态算法的选择,因此其功能复杂,程序冗长。程序模块化后可有效提高工作效率,操作简便。探讨利用嵌入式软件模块化的方法,基于ARM平台根据嵌入式测姿系统软件的主要流程及其功能对软件进行单元划分,详细阐述了各个模块的功能以及模块之间的接口,解决可操作性、可扩展性等问题,实现了软件的模块化设计。实际数据验证表明,嵌入式测姿软件模块化后可移植性、扩展性增强,可用性高,资源利用率高,并适合在一般载体上使用。     

基于脉冲位置幅度调制的距离速度同时测量

针对传统波形方法在多普勒激光雷达测量目标距离和速度的应用中不能同时获得高测量精度的问题,提出一种使用位置和幅度同时调制的测量信号波形,以解决距离和速度测量精度之间的矛盾,同时使两个参数测量之间相互独立,并分析了该方法应用于智能驾驶道路环境中目标距离和速度测量的可行性.首先,讨论典型调制方法在同时测量目标距离和速度方面存...     

基于GPU加速遗传算法的直接定位研究

针对大规模数据下遗传直接定位算法执行时间慢、实时性较差的问题,提出了基于GPU加速的并行遗传直接定位算法。根据直接定位代价函数特点,设计了GPU高速并行遗传进化架构,通过对适应度函数并行化计算以及对选择、交叉、变异等遗传操作并行化设计,缩短了算法执行时间,提高了算法执行效率。仿真实验表明,通过合理的GPU并行线程结构设计,显著提升了遗传直接定位算法的执行速度,可更快得到直接定位估计结果。