嵌入式操作系统的形式化验证方法

对嵌入式操作系统类安全关键软件,测试、模拟、分析等传统软件验证方法不能保证其正确性,需要使用形式化方法。综述了主流商用嵌入式操作系统所采用的形式化验证方法,分析了操作系统内核不同特性的形式化验证思路。通常对空间隔离、信息流控制、系统调用、进程间通信等的证明采用定理证明方式,而对时间隔离的证明则采用模型检测方式。 seL4的通用抽象和逐层精化方法、模型检测和定理证明的混合方法在工程使用中都有前途。     

基于NuSMV的AADL模型形式化验证技术

结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言，在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性，提出基于NuSMV(新符号模型检查器)的AADL模型形式化验证方法。首先，覆盖AADL模型的所有软件构件和行为特征，提出了AADL模型到NuSMV模型的映射规则和转换算法；其次，采用图同构方法分析了转换算法的正确性；然后，在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述，以验证AADL模型中安全性、活性和嵌套模态配置的正确性；最后，以飞行控制系统为例，详细阐释了基于NuSMV的AADL模型形式化验证方法，并给出验证属性的统计信息。     

系统形式化分析在AILS研发中的应用

系统形式化分析（system formal analysis）是近些年在航空系统研发中所应用的一种安全评价方法。原理是运用数学建模，对研发航空软件系统所有假设条件下的输入集元素的有效性及系统算法逻辑性进行验证，其本质是假设合理性及算法正确性的数学检验，可弥补传统的模拟、试飞等安全评价手段的局限性，并将逐步成为未来航空系统研发中安全评价的重要步骤和手段。介绍了系统形式化分析在机载横向间隔信息系统（AILS）研发中的安全评价应用，通过假设检验、建模验证AILS告警算法等，给出了该系统的安全性论断并提出了相关建议。     

基于SCADE的FADEC软件通用基准模型库开发

在航空发动机全权限数字电子控制（FADEC）软件研制过程中,可重用基准模型库的开发和使用是提升软件研发效率和 质量的重要技术手段。为了提升FADEC软件复用效率,加快软件研发进程和适航认证,在分析模型库相关指南和规范的基础上, 结合工程实际的需要,完成FADEC基准模型库的设计和验证,以三角函数类、方根类、滤波类和余度表决类4种典型类型为对象, 通过泰勒定理、牛顿迭代和离散化等数学理论和自动控制理论进行机理分析,基于安全关键软件开发环境（SCADE）建模仿真工具 完成模型库设计,通过对比仿真、模型测试和形式化验证方法等完成模型库验证。结果表明：该基准库支撑了多个FADEC软件项 目的研制,其正确性和可靠性已在各项工程试验中得到反复检验,具有十分重要的工程价值,所提出的模型库设计和验证方法也 具有一定的借鉴意义。     

符合民机适航标准的形式化方法研究

描述了形式化方法的定义、目的、作用和软件开发流程。以发动机仪表盘显示布局风格需求为例,通过四变量形式化方法对需求进行形式化建模,通过形式化分析证明模型的完备性和一致性。以发动机油量周期计算需求为例,通过Event-B形式化方法对需求进行形式化建模,通过形式化分析发现需求模型的缺陷。对民机适航标准形式化方法相关的三份补充文件进行了解读,对采用形式化方法进行民机软件开发具有指导意义。     

MILS机载安全操作系统设计

针对构建MILS安全嵌入式操作系统需求,提出一种基于微内核的安全机制。通过微内核的安全监控机制和时空隔离结构,为系统提供安全性和可靠性的基础支撑,避免操作系统中访问控制机制被篡改、绕过,采用任务间时空隔离和消息传递机制使得各个安全关键任务独立运行,通过受控的消息机制进行交互,有效保证了各个模块的独立安全性。采用微内核架构能够进一步形式化验证,从而在安全的系统结构的下提高任务的安全性和可靠性。     

嵌入式多核操作系统确定性研究

为解决嵌入式多核操作系统确定性问题,详细阐述了计算确定性,重点分析了多核结构引入的不确定性问题。通过研究嵌入式多核操作系统的结构,从共享存储的确定性访问、确定性任务调度、确定性通信等方面提出了解决多核结构带来的不确定性问题的方法。     

一种基于AADL的航空电子系统仿真和验证技术

飞机系统集成化程度的提高增加了对航空电子系统设计和分析的难度,同时也对安全性需求等系统特性的验证提出了更高的技术要求。对基于结构化分析和设计语言(AADL)的系统建模和仿真流程及相应的评估分析能力进行了介绍,并在基于AADL的航空电子系统建模框架下,提出基于AADL的航空电子系统仿真评估和验证方法,利用结构化分析和设计语言AADL构建航空电子系统典型子系统的正常模型和错误模型,并以此建立系统的扩展模型。在此基础上,利用形式化方法对系统模型进行描述并转化为Kripke结构。最后对系统模型进行模型仿真和特性验证,验证所构建的系统架构和设计逻辑是否符合系统设计特性需求。     

基于机载多核弱序存储模型的共享内存驱动软件设计方法研究

随着航空电子系统承载的应用日趋复杂,飞机对机载计算机的计算力和功耗比要求不断提升,这也推动了嵌入式多核处理器的加速应用和普及。多核处理器在航空电子设备的深入应用,随之而来的是运行其上的软件复杂度急剧上升,面向应用的航电系统设计面临挑战。多核处理器平台由于需要面对并行、指令乱序、资源共享冲突等问题,而目前国内大多数机载嵌入式软件和驱动仍然是基于单核处理器设计和实现的,影响最大的是在机载嵌入式实时操作系统环境下的驱动软件,因此需要充分考虑多核带来的各方面影响,尤其是需要兼顾共享内存等资源的使用冲突和实时高效要求。本文结合机载航电多核处理平台的特点,提出了一种基于机载多核弱序存储模型的共享内存驱动软件设计方法,并基于该方法设计了FC总线驱动和MBI总线驱动,项目应用结果表明,设计的驱动程序在多核处理器平台上数据传输正确,验证了方法的正确性和有效性。     

航空电子嵌入式计算建模仿真方法研究

航空电子系统经过数十年的演进,正朝着更加开放、灵活、智能的方向发展,同时也不断面临新的问题和挑战,需要在功能复杂度不断提升的前提下实现资源的高效分配,保证系统的实时性与可靠性。通过分析机载嵌入式计算特点,基于模型的系统工程理论的同时结合形式化建模仿真方法,针对典型嵌入式计算平台场景中的组件开展基于模型的设计方法研究与应用。该方法能够清晰描述航电嵌入式计算的时间关键性特征,有效辅助设计和论证工作,降低研发周期、提升设计的可复用性。     

面向空管安全系统中人为因素的本体建模分析

人为因素在空管安全系统中是导致不安全事件发生的关键因素;本体作为一种概念化的明确的规范说明,是对客观存在的概念和关系的描述,本研究将本体建模引入空管安全系统中,提出了一种基于本体的提取关键因素的分析方法,对影响空管安全的关键因素——人为因素,进行了本体形式化的描述,构建了人为因素本体模型,并通过实验对不安全事件中的人为差错进行本体模型分析;通过本体建模挖掘出不安全事件内在的、隐舍的逻辑关系,从而为降低或避免不安全事件的发生提供了科学依据。     

一种多核分区操作系统的绑定组调度方法

伴随机载计算平台对算力提升的显著需求,综合化模块化航空电子系统(IMA)采用多核处理器和相应的多核分区操作系统成为必然趋势,从而对目前仅适用于单核处理模式的多分区调度算法产生了进一步的能力扩展需求。面向多核处理的多分区调度算法需要在发挥多核处理效能的同时,继续维持机载安全关键系统的实时性和确定性特征。为此,提出一种基于...     

模型驱动的安全关键系统标准符合性验证方法

大部分安全关键系统都需要进行安全认证,以确保其不会对人、财产或环境造成重大伤害。提供符合性认证所必须的证据是一项具有挑战性的任务。目前学术界提出一种模型驱动的安全关键系统标准符合性验证方法,该方法便于证据链的收集和标准符合性验证。分析了当前模型驱动的安全关键系统的研究现状,介绍了其标准符合性验证方法的概念、模型和框架,并将其与传统的方法进行比较分析,为我国安全关键系统的标准符合性验证提供借鉴。     

基于同步语言SIGNAL的一种系统设计方法

简要介绍同步语言SIGNAL,并讨论了一种在POLYCHRONY平台下的嵌入式系统设计方法,同时以有限LIFO堆栈为例进行说明。方法主要是利用SIGNAL进行组件建模,它强调把形式化技术放到验证、分析以及代码生成中。     

千兆三余度AFDX 帧管理的形式化建模与验证

为了提升新一代航空电子全双工交换以太网（AFDX）网络的传输速率和余度设计可靠性,在AFDX 网络标准的基础上（ARINC 664 p7）,建立千兆三余度AFDX 网络的帧管理机制模型并进行了形式化建模, 而且实现了AFDX 网络标准中描述的SkewMax 机制。使用UPPAAL 形式化工具对千兆三余度AFDX 网络帧 管理机制进行形式化验证,验证帧管理机制的完整性检查及冗余管理功能的可用性。结果表明,千兆三余度 AFDX 网络帧传输过程中不存在死锁。此外,针对标准AFDX 的冗余管理中一个帧的丢失可能会导致其冗余备 份的丢失的现象,提出在接收端设置一个队列,记录那些比连续帧更晚到达的冗余备份的帧序号,从而减少不 必要的丢帧,提高QoS 和数据完整性。形式化验证的结果可以作为千兆AFDX 网络标准制定和实际应用的参考。     

SDL在空间通信协议开发中的应用

针对空间通信协议开发难度大、代价大的问题,提出了基于协议工程思想利用SDL(规范与描述语言)对SCPS-TP(空间通信协议规范-传输协议)进行开发的方法,包括SDL建模、仿真和验证。首先对SCPS-TP进行了功能分析,确定功能点和状态机,并据此利用SDL建模;接着对模型进行实时仿真,测试其正确性,通过调试保证所有功能通过仿真;最后对模型进行了验证。验证结果表明,SCPS-TP不存在死锁、活锁等逻辑错误,为其在空间通信中的应用提供了有力支持,同时也说明了SDL在空间通信协议开发中的重要应用。     

飞行员操作程序的形式化描述

本文提出用状态转移表这种形式化方法描述飞行员操作程序,并在此基础上开发了POP测试用例标准解生成软件。用形式化方法描述飞行员操作程序,可以向系统软件设计者提供完备的、一致的和严密的软件需求规范,可用软件工具进行自动处理。     

基于STPA的飞机交流系统供电转换安全性分析方法研究

飞机交流发电系统是整机的主要电力来源,应对其进行完善的安全性分析。传统安全性分析方法对系统组件间非线性交互引起的安全问题关注较少,当研制型号支持数据不足时,存在分析遗漏风险。根据典型交流发电系统供电转换过程基本特点,基于STPA方法构建安全控制结构图,识别不安全控制行为（UCA）,引入相似系统的失效模式及影响分析（FMEA）结果,分析UCA致因因素和致因场景,使用时间自动机理论的形式化工具进行系统建模与验证;通过专家评判及事故对比来验证该方法的正确性。结果表明：在传统分析方法的基础上引入STPA方法,能够有效识别出不安全控制行为和事故发生的原因,该方法可以作为传统方法的有效补充。     

嵌入式分区操作系统可靠性技术的研究与应用

嵌入式实时多分区操作系统是专门为新一代航空电子系统开发的,是支持综合化航空电子系统的嵌入式实时操作系统,该操作系统是基于分区的高安全、高可靠操作系统,其可靠性决定了运行在其上的应用软件的可靠性。从软件可靠性概念着手,深入研究了嵌入式实时多分区操作系统开发过程中涉及的可靠性设计技术,给出了软件可靠性应用的示例,并研究了操作系统软件研发中使用的可靠性管理方法,对软件的可靠性进行了总结。     

机载分区操作系统形式化建模及验证研究

分析和总结了国内外在机载分区操作系统建模及验证方面的研究成果,指出了存在着验证工作不充分性、建模与验证方法单一性等问题;提出了从"设计后验证"到"Correct-by-Construct"、从规约模型到契约模型、组合运用多种形式化建模三种分区操作系统建模及验证的新思路,以期对未来研究者有所借鉴。