共查询到19条相似文献,搜索用时 109 毫秒
1.
为保证SCADE软件开发的安全性,研究了SCADE形式化验证技术,指出其不足,提出了基于代码生成器的解决方法.该方法对安全特性属性引入了逻辑描述,并利用SCADE编辑器及代码生成器的特点,对SCADE形式化验证技术进行改进,降低了模型正确性确认时人为的主观性.通过实例阐述了应用该方法进行形式化验证的一般步骤,表明了该方法是有效可行的. 相似文献
2.
3.
随着航空电子软件的迅速发展,传统的软件设计方法已不能满足其效率和安全性需求.为解决传统设计方法的不足,寻求一种更有效的控制软件设计方法,高安全应用开发环境SCADE应运而生.主要介绍了高安全应用开发环境SCADE的开发背景及开发特点,并以飞机飞行控制律为例,按照SCADE软件的程序设计流程,即通过直观的图形化建模建立无人机飞行控制律模型,通过模拟仿真保证设计的正确性,最终自动生成可直接面向工程的嵌入式C代码.实验结果表明,SCADE在很大程度上实现了软件开发的自动化,节约了开发成本和开发时间,体现了SCADE环境下进行软件开发的优越性. 相似文献
4.
现有磁浮列车测速定位系统所采用的技术比较单一,测速定位系统的可靠性不足,不能更好地满足各种运行环境的要求。通过分析现有磁浮列车测速定位技术的优缺点,提出了一种新型测速定位系统模型,系统模型以传感器定位技术、多普勒雷达定位技术、查询应答器定位技术为基础,通过组合逻辑对系统数据进行优化。系统模型较现有技术具有高精度、高可靠性、易工程化等优点,同时采用安全性软件开发工具SCADE对系统模型进行建模及形式化验证,验证结果表明系统模型满足设计要求。 相似文献
5.
6.
本文介绍了一种基于单片机技术和光电传感器技术开发的新型列车测速系统,它区别于传统的通过测量转速和利用GPS测算列车速度的方法。本系统通过测量列车行驶在轨道上单位时间内通过的枕木个数来计算列车的运行速度。 相似文献
7.
8.
9.
基于场景分析的系统形式化模型生成方法 总被引:1,自引:0,他引:1
采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。 相似文献
10.
针对卡口环境下视频测速误差大的问题,提出一种提高测速精度的方法。采用以车牌第2个字符作为车辆定位的特征块,利用小波变换分解字符的外部边界特征曲线,在低分辨率下实现目标字符的模板匹配,并获取该曲线相对模板的偏移量,在原分辨率上进行边界坐标的精细调整,完成车辆特征块的精确定位。结合字符高度固定的先验知识,确定车辆特征块所处的实际坐标系,以提高对车辆行驶距离的计算。在实际环境下,对该方法进行长达2个多小时的测试,并对测试结果与线圈测速、基于车牌定位的视频测速进行对比,结果表明,在车辆正常行驶的速度下,与线圈测速相比,该方法视频测速误差在3 km/h以内。 相似文献
11.
基于代数的软件过程建模系统的设计与实现 总被引:1,自引:0,他引:1
软件过程建模的主要目的是建立组织内软件开发过程的模型,使得软件开发过程在整个组织内获得一致的理解,进而提高软件开发效率和改进软件生产质量.软件过程建模语言一方面要易于理解、具有较强的表达能力,同时也要易于分析和验证,以保证所要描述的软件过程的正确性.介绍了基于代数的软件过程建模系统ASPMS的设计和实现,该系统提供了图形化的建模表示方式,而该图形化表示方式具有基于多元π演算的形式化语义,从而较好地平衡了建模语言的易于理解、具有较强的表达能力和易于分析和验证这一矛盾的内在要求. 相似文献
12.
13.
14.
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. 相似文献
15.
为了系统高效地分析固件中潜在的安全隐患,提出了一种基于行为时序逻辑 TLA 的软硬件协同形式验证方法。通过对固件工作过程中的软硬件交互机制进行形式建模分析,在动态调整攻击模型的基础上,发现了固件更新过程中存在的安全漏洞,并通过实验证实了该漏洞的存在,从而证明了形式验证方法的可靠性。 相似文献
16.
17.
嵌入式测姿系统软件的模块化 总被引:1,自引:1,他引:1
由于嵌入式测姿系统软件根据不用需求需实现多种接收机板卡、不同导航系统、多种姿态算法的选择,因此其功能复杂,程序冗长。程序模块化后可有效提高工作效率,操作简便。探讨利用嵌入式软件模块化的方法,基于ARM平台根据嵌入式测姿系统软件的主要流程及其功能对软件进行单元划分,详细阐述了各个模块的功能以及模块之间的接口,解决可操作性、可扩展性等问题,实现了软件的模块化设计。实际数据验证表明,嵌入式测姿软件模块化后可移植性、扩展性增强,可用性高,资源利用率高,并适合在一般载体上使用。 相似文献
18.