共查询到20条相似文献,搜索用时 78 毫秒
1.
2.
3.
基于NuSMV的AADL模型形式化验证技术 总被引:1,自引:0,他引:1
结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性,提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先,覆盖AADL模型的所有软件构件和行为特征,提出了AADL模型到NuSMV模型的映射规则和转换算法;其次,采用图同构方法分析了转换算法的正确性;然后,在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述,以验证AADL模型中安全性、活性和嵌套模态配置的正确性;最后,以飞行控制系统为例,详细阐释了基于NuSMV的AADL模型形式化验证方法,并给出验证属性的统计信息。 相似文献
4.
在航空发动机全权限数字电子控制(FADEC)软件研制过程中,可重用基准模型库的开发和使用是提升软件研发效率和
质量的重要技术手段。为了提升FADEC软件复用效率,加快软件研发进程和适航认证,在分析模型库相关指南和规范的基础上,
结合工程实际的需要,完成FADEC基准模型库的设计和验证,以三角函数类、方根类、滤波类和余度表决类4种典型类型为对象,
通过泰勒定理、牛顿迭代和离散化等数学理论和自动控制理论进行机理分析,基于安全关键软件开发环境(SCADE)建模仿真工具
完成模型库设计,通过对比仿真、模型测试和形式化验证方法等完成模型库验证。结果表明:该基准库支撑了多个FADEC软件项
目的研制,其正确性和可靠性已在各项工程试验中得到反复检验,具有十分重要的工程价值,所提出的模型库设计和验证方法也
具有一定的借鉴意义。 相似文献
5.
时间触发以太网拜占庭容错方法的形式化验证 总被引:1,自引:0,他引:1
对于时间触发以太网的拜占庭容错方法,已有的推理性论证表明网络的分布式时钟同步机制有利于容错过程中实现交互一致性。为对该容错方法的正确性进行严格验证,进一步采用模型检查的形式化分析手段,通过符号分析实验室(SAL)形式化工具,构建了网络节点模型,建立了时间触发体系结构下的拜占庭容错场景,设定了容错操作活性、一致性和有效性等属性的形式化定理。模型检查的结果表明:在三冗余独立路径条件下,该方法可以容忍一个拜占庭故障,且在存在指令/监视对(COM/MON pair)的条件下可以容忍2个高完整性配置节点的"不一致遗漏"故障。与推理论证手段相比,SAL模型检查为时间触发交换式网络在航空航天高安全关键等级系统中的容错配置提供了更规范的依据。 相似文献
6.
UML是一种可视化的图形语言,已成为面向对象方法中事实上的工业标准,得到了广泛应用.但是UML缺乏精确的语义描述,不便于使用工具对其进行分析和验证.形式化B方法基于严格的数学理论,按照抽象机的方式理解系统.为了使UML表达的语义更加明确,同时发挥形式化方法的优势,采用B方法对UML中的顺序图进行描述. 相似文献
7.
结构覆盖率分析是基于需求测试的补充和完善,能够发现软件中是否存在预期外的功能.在基于模型的软件开发过程中,模型覆盖率代替了传统的代码覆盖率,运用模型检查技术自动生成测试用例是形式化方法在模型覆盖率测试中的主要途径,涵盖了判定覆盖(DC)、条件覆盖(CC)、修改条件/判定覆盖(MC/DC)等多种方式.以航空发动机FADEC软件开发过程中的一个实际案例为例,结合Simulink Design Verifier分析验证工具,检验其生成的用例对模型的覆盖率,表明方法的实用性. 相似文献
8.
9.
10.
固态功率控制器是飞机配电系统的重要组成部分,是固态配电的核心,需要在系统研制过程中进行完善的风险识别与安全性分析。当今使用较多的方法如故障树分析等主要基于部件独立性计算系统失效率,但针对组件之间非线性交互带来的安全性问题的研究较少。为此以固态功率控制器为对象,应用STPA方法识别不安全控制行为,利用UPPAAL工具建立形式化模型并对不安全控制行为进行验证,基于过程模型识别危害场景并进行形式化验证,形成更详细的SSPC安全控制约束清单。结果表明,方法可以有效识别出SSPC组件交互不当产生的安全性问题。 相似文献
11.
面向应用的嵌入式操作系统 总被引:4,自引:0,他引:4
讨论了经典的实时操作系统RTOS在嵌入式DSP和嵌入式Internet应用中的不适应性 ,提出了具有可伸缩性、可剪载性、具有强大主机开发支持能力以及面向应用特点的嵌入式实时操作系统的思想 ,并介绍了两种实际产品的特点和使用情况。 相似文献
12.
嵌入式系统--后PC机时代 总被引:1,自引:0,他引:1
在以PC为代表的通用计算机系统出现了发展减缓的趋势之后,嵌入式系统逐渐在信息电器、智能家电等方面有了大发展,本文详细介绍了嵌入式系统的特点及应用. 相似文献
13.
机载嵌入式软件可靠性设计研究 总被引:1,自引:1,他引:0
机载航电系统的可靠性问题越来越受到关注,软件可靠性设计要抓住两个方面,软件开发过程和软件开发方法。本文根据机载嵌入式系统软件的特点,讨论了软件开发过程在可靠性方面的考虑,还有在需求、设计、编码阶段使用的相关设计方法和技术。 相似文献
14.
如何进行嵌入式软件的覆盖测试和性能测试,是嵌入式软件测试工程师较为关心的热点问题之一。介绍了一种基于PowerPc755目标板的嵌入式软件覆盖和分析测试方法。方法借助于嵌入式软件测试工具TestBed和实时硬件数据采集工具RTInsight,搭建了嵌入式软件动态测试平台,并在该嵌入式软件动态测试平台上进行了覆盖测试和性能测试,同时给出了相关的覆盖率测试和时间性能测试的测试结果。 相似文献
15.
16.
性能评测是查找嵌入式计算机系统性能瓶颈、指导设备选型、平衡相关部件、优化系统结构以及提高系统实际性能的重要方法。在介绍了机载嵌入式计算机系统性能评测的指标和基本方法之后,重点分析了使用基准测试程序的测试方法和特点,以及基准测试方法的对比测试原理、不同测试环境的构建以及主要测试过程;选取了SPEC CPU 2000基准测试程序集针对机载嵌入式环境进行裁剪和移植,对某国产机载嵌入式实时操作系统分别以不同的嵌入式操作系统、嵌入式文件系统和编译选项为变量参数进行对比测试,得出了国产操作系统与国外同类商用操作系统运行实际应用程序的性能基本相当的结论,另外也得出文件系统对计算类基准程序的结果影响较小以及编译优化后能够大幅提高嵌入式系统性能等结论。 相似文献
17.
18.
19.