基于Event B的中断管理需求和设计形式化建模与验证方法

随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.     

基于有限状态机的操作系统需求层形式化验证

操作系统是航天器必备的基本软件，操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障，但仍存在不能完全排除缺陷的情况，因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分，本文在分析操作系统需求的基础上，采用有限状态机在操作系统需求层进行形式化描述，并针对应用在某航天器上的SpaceOS2在需求层进行了建模，相应地在定理证明工具Coq中进行了描述建模；然后定义了六条操作系统应满足的全局性质并进行了形式化描述，给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的，为进一步全面形式化验证奠定了基础.     

基于Kalman滤波的GPS跟踪环路晶振闪烁噪声建模方法

由于晶振频率漂移对GPS接收机的载波相位和频率跟踪带来了误差,在载波跟踪系统中需要对晶振误差进行建模。传统基于Kalman滤波的跟踪方法无法对非白的闪烁晶振误差进行准确建模,导致跟踪环路建模产生一定的误差。针对上述问题,文章重点分析了晶振的频域模型建模过程和噪声协方差求解问题,提出了Kalman滤波中晶振闪烁噪声的近似建模方法,并用实际卫星数据验证了建模的正确性。     

基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法 Event-B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模,依靠不变式来保证模型的正确性,并且在Rodin平台上对模型进行了形式化验证,结果表明模型是正确的.     

虚拟化技术在综合化航电系统中的应用

将虚拟化技术应用于航空电子系统的设计,利用虚拟机系统来实现硬件资源的共享管理和软件子系统的划分,并符合ARINC 653规范的要求——模块化、可靠性、隔离性与开放性.构建由硬件平台、虚拟机监视器(VMM,Virtual Machine Monitor)和分区操作系统、航电应用软件所组成的3层软件架构,可以满足综合模块化航电系统(IMA,Integrated Modular Avionics)的功能要求与接口要求.其中,为实现符合ARINC 653要求的VMM,传统分区操作系统需要进行多项关键性调整,包括处理器特权级和特权指令、中断、内存地址空间分配、设备驱动等方面,从而可以构造基于VMM的综合化航空电子系统.     

操作系统共享数据临界保护正确性测试方法

研究了共享数据临界保护正确性测试,提出一种基于共享数据地址监控的临界保护正确性测试方法(SVAM,Shared Variable Address Monitor).SVAM由实时地址监控模块和共享变量地址列表组成.当系统运行时,SVAM在地址总线上实时监测共享变量的写操作,当系统在更新共享变量值时没有关闭中断说明对该变量的操作破坏了临界保护,存在运行风险.理论分析证明了SVAM的正确性,仿真试验证明了该方法的有效性.      

虚拟维修仿真建模与控制实现

现有的建模技术在描述维修过程及其相关信息资源等方面存在很大不足,同时缺乏将抽象的维修任务描述与底层维修活动仿真相结合的研究,针对此问题提出并建立了维修任务仿真管理模型 MTN(Maintenance Task Net).构建MTN模型框架并建立基本功能模块,同时阐述了MTN建模的3个要素:状态、活动和条件.基于状态描述各种维修资源,基于活动定义维修动作行为,基于条件建立资源与活动间约束关系.进一步阐述MTN驱动虚拟场景进行维修仿真,同时控制管理整个维修仿真过程.最后给出了应用实例,该模型对实际工程中维修工作分析评价的开展具有一定的实用价值.      

基于拜占庭容错体系构架的航天器控制系统测试性设计与分析

摘要： 飞行控制系统作为航天飞行器的关键机载系统,其运行情况直接关系到飞行任务的成败.通过良好的测试性设计,可以提高系统的可靠性和安全性,减少维修人力及其他保障资源,降低寿命周期费用.对拜占庭容错体系结构的航天器控制系统和分层多信号流图模型的测试性设计和建模方法进行了详细的叙述,并对基于拜占庭容错体系结构的航天器控制系统进行了测试性建模,通过测试性建模和分析系统（TMAS软件）验证控制系统测试性设计的正确性和有效性.     

Udimet 720 Li材料B-P型粘塑性本构建模研究

针对航空发动机用涡轮盘材料Udimet 720 Li,根据高温单轴实验结果,对其在各种载荷条件下的力学行为,开展了采用Bodner-Partom(B-P)统一型弹-粘塑性本构方程进行建模的研究.充分讨论了基于内变量理论的该型本构模型对率相关拉伸、循环硬化及蠕变等力学行为同时进行建模的能力;根据对模型的本构分析,给出了一种分类加整体考虑的模型参数优化策略.通过ABAQUS用户子程序,把该模型结合进了有限元方法,并进行了计算验证.研究表明B-P本构模型可较好地建模高温镍基合金Udimet 720 Li的各种力学行为.      

混响载荷的建模方法及其空间相关性影响研究

针对航天器混响声场中的声振预示问题,提出了一种满足声场载荷空间相关性的混响载荷建模方法,该方法能够简化声振分析的建模过程,提高分析效率。首先基于波动理论给出了混响载荷空间相关性的理论模型;随后结合工程需求,提出了基于Rayleigh积分和互易关系的混响载荷建模方法,并从理论上证明其满足混响载荷的空间相关性理论模型;最后采用典型算例对建模方法的正确性进行了验证,并研究了声场载荷空间相关性对声振预示结果的影响。     

考虑温度影响的干摩擦接触分子动力学研究

基于多尺度方法对干摩擦行为进行预测已成为当前研究热点。对于航空发动机等高温机械系统，温度对干摩擦行为影响至关重要。针对高温影响下微动界面摩擦行为开展分子动力学建模与分析，研究不同温度下微凸体的切向碰撞过程；考虑温度的升高使摩擦界面微凸体黏着作用增强，提出不同于赫兹接触理论预测的真实面积计算方法；基于所建的分子动力学模型和G-W接触模型，研究不同温度下接触面的摩擦系数，与实验测量的摩擦系数结果吻合，验证所提方法的正确性。对于在高温环境下接触、摩擦及微动等界面力学问题的研究提供了可借鉴的方法，同时为高温旋转机械动力学多尺度方法提供了可参考的解决手段。     

基于向量对方法的柔性空间机械臂建模与仿真

针对柔性自由漂浮基座空间机械臂系统建模的过程中存在的形式复杂计算量大等问题,本文采用向量对方法,以自由漂浮基座双连杆柔性机械臂为研究对象,以单个体的动力学方程为基础,分别列出相邻两个体之间的约束方程,利用拉格朗日乘子法组装构成系统的动力学方程.这种方法在建模时需要的信息较少,易于推导,得到的方程十分规范化,更加有利于柔性空间机械臂控制系统的设计.最后文章通过仿真验证了模型的正确性.     

飞机制造工装中典型配套结构自动建模技术

飞机制造工装中存在大量配套结构,其中各元件在空间方位和结构尺寸等方面具有严格的关联关系,但这些元件并不总是构成一个完整的组合件,而是独立隶属于工装总体结构.现有的配套结构建模技术需要繁琐的人工操作,为了实现这类结构的自动建模,提出了基于结构关联关系的虚配件技术.首先,根据配套结构的构成元件间的依赖关系引入虚配件的概念,并以此为基础对配套结构进行了形式化定义和表示;其次,研究和建立了配套结构自动建模原理,并对其中涉及的语义模型解释、文档创建及子件安装等关键算法进行了详细说明;最后,通过V形块组件结构实例测试,验证了所提方法的正确性和有效性.     

DS/FH测控系统抗干扰性能分析与测试

为全面、有效衡量用于应急测控的直扩/跳扩(DS/FH)系统的综合抗干扰性能,采用最低性能指标约束法,对系统抗干扰性能进行综合分析.以音调干扰、脉冲干扰以及高动态环境为例,探讨了不同干扰条件对系统最低性能指标的影响.为解决最低性能指标约束下系统抗干扰性能测试步骤繁多、效率低、代价高的不足,采用蚁群算法,将指标测试次序建模为最佳路径选择问题.通过实例仿真验证了测试模型的正确性与有效性.该方法对DS/FH测试方案的选择具有指导意义.      

基于FFS故障行为模型的等效故障注入方法

针对测试性验证试验中部分故障模式不可注入,或注入后易导致装备出现不可修复的损坏等问题,提出了基于“故障模式-功能-状态”（FFS）故障行为模型的等效故障注入方法。首先,对FFS总体建模思路进行了描述,提出将“功能”作为基本建模要素,在分析装备自身多元建模信息的基础上,建立了故障行为模型。其次,对各相关矩阵和行为状态向量进行了定义,研究了故障模式、功能、状态间的不确定信息表征方法,提出了故障模式-状态相关矩阵的求解方法。最后,给出了等效故障模式的定义和基于FFS故障行为模型的等效故障注入流程。将所提方法应用于某装备发射控制系统,结果表明,所提方法能够实现等效故障注入,故障注入率提高约16.7%。      

航天器在轨角动量演化及卸载策略研究

为了减少在轨卫星的喷气卸载次数,节省推进剂,延长卫星的使用寿命,对地球静止轨道零动量卫星和V型轮偏置动量卫星的角动量管理问题进行了研究.根据卫星角动量累计演化特点,给出两类卫星的角动量管理方法,提出优化的喷气卸载策略.基于上述研究对在轨卫星非正常卸载情况进行了理论分析与仿真验证,提出解决措施.在轨试验表明,基于优化的喷气卸载策略进行卫星角动量管理,可明显减少卫星的卸载次数,验证了策略的正确性.     

基于Patran/Nastran的结构优化系统的工程应用

采用基于有限元软件Patran/Nastran二次开发的结构优化系统,对两个卫星结构进行了以重量为目标、考虑基频和应力等约束的优化设计.系统由用户在Patran环境下完成问题建模,优化过程中调用Nastran作结构分析并结合二级多点逼近算法寻优.设计对象是由蜂窝夹层板、不同截面形状梁、板壳等组成的典型复杂航天器结构,设计过程中还利用人机交互技术,最终使重量明显降低,为工程部门改进设计提供了依据.算例结果之一与其他结构优化系统结果一致,进一步说明了所开发系统的正确性.     

Udimet 720 Li 高温变形特性的粘塑性本构建模研究

采用Chaboche统一粘塑性本构方程,对Udimet 720 Li在700℃时的单调拉伸、循环加载及蠕变特性等复杂的高温变形现象进行了建模研究.探讨了Chaboche本构理论对这些变形现象进行建模的形式,并特别针对快速各向同性软化和非对称循环加载时的平均应力松弛现象,对Chaboche本构理论进行了修正和变化.将经过修正的Chaboche本构理论,与Levenberg-Marquadt非线性优化算法相结合,编制了材料参数优化程序,得到了材料参数值.研究表明,经过修正的Chaboche本构模型可较好地建模镍基高温合金Udimet 720 Li在高温下的各种变形行为.      

一种运载火箭用大功率电动伺服驱动器的散热设计

散热对电子设备的性能有着直接的影响,散热器广泛应用于电子产品的热设计用于改善其散热能力,因此散热器应作为关键部件进行设计。针对航天领域使用的大功率电动伺服驱动器的散热问题,提出了通过热力学理论计算指导散热器结构设计的方法。首先通过理论计算结果确定散热器的结构尺寸,然后通过PRO/E三维建模软件对散热器进行建模并利用ANYSY ICEPAK热仿真软件对所设计的散热器进行热仿真,最后搭建了伺服驱动器的热试验环境。仿真结果和试验数据均验证了该设计方法的正确性。