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

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

基于本体的软件安全性需求建模和验证

由软件引起的灾难性事故原因往往源于安全性需求,目前主观的人工评审方法并不能满足软件安全性需求严格的验证要求.因此,讨论了软件安全性需求的定义,遴选了国内外公认的相关标准和手册作为需求验证的知识基础,根据"七步法"建立了本体模型,利用本体模型中的概念和关联来形式化地描述规则以支持验证;同时基于以上研究内容设计和实现了软件安全性需求形式化建模和验证的工具原型,并对使用工具实施验证和使用人工评审实施验证进行了对比分析实验.实验结果表明形式化工具原型在验证时间和验证次数上都大大优于人工验证方法,同时工具原型具有良好的易用性.     

组合服务控制流测试

结合Web服务本体语言(OWL-S,Web Ontology Language for Services)和线性时态逻辑理论(LTL, Linear Temporal Logic),研究用于测试的组合服务流程形式化描述方法和动态测试信息分析方法.将OWL-S作为组合服务的需求参考模型,采用组合服务标准和形式化描述方法相结合的方式,用线性时态逻辑刻画OWL-S控制结构的动态语义,明确地表示出控制结构中各成分的执行顺序.进一步用线性时态逻辑公式集合描述组合服务的控制流需求,从而使原子服务的交互模式有了明确的表示.基于这种交互模式表示,采用LTL在有限状态序列上的语义,对组合服务实现执行过程中获取的动态信息进行分析,测试组合服务实现的执行过程与组合服务控制流需求的一致性.     

基于顺序失效符的动态故障树形式规约

首先定义了顺序失效符(SFS,Sequence Failure Symbol)的形式化框架,包括SFS定义、性质、规则和定理,这是动态故障树(DFT,Dynamic Fault Tree)形式规约的基础.然后给出了任意形式的静态故障树(SFT,Static Fault Tree)和DFT在SFS形式化框架下的形式规约方式和自动转换算法.最后,通过示例验证了方法的有效性.形式规约构建了DFT在数学层面上更加严密的理论体系,同时,基于SFS的形式规约自动转换算法有助于DFT计算机辅助建模的实现.     

密码协议的分层安全需求及验证

将密码协议的安全需求分为浅层需求和深层需求2个层面,阐述了密码协议的分层安全需求.采用近世代数和时序逻辑的方法定义了形式化描述语言,并形式化地描述了密码协议的分层安全需求.将类BAN逻辑与模型检查相结合,在Abadi-Tuttle模型的基础上建立密码协议的计算模型.以Otway-Rees协议为例,利用该计算模型和定理证明技术对密码协议进行了多层需求验证.     

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

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

基于多星联合侦察的卫星数传调度问题模型

基于多星联合侦察的卫星数传调度问题是研究如何为卫星数传任务中每个单数传任务分配地面资源及数传时间的问题,对该问题的模型进行了研究.首先建立了单数传任务模型及卫星数传任务模型;然后在此基础上建立了问题的约束满足优化模型,重点分析了问题的目标函数及主要约束条件;为了解决该问题,最后提出了一个基于双综合优先度的启发式调度算法,并通过实例验证了算法的有效性.研究成果实现了问题的形式化描述,并给出了一种有效的问题求解算法.      

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

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

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

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

一种新的自适应模糊控制器的设计方法

在分析现有的自适应模糊控制器不足之处的基础上,提出了一种新的自适应模糊控制器设计方法.为保证系统性能的一致性,在启动自适应模糊控制器前,采用监督控制将初始跟踪误差镇定到给定范围.自适应模糊控制器可在存在模糊逻辑系统逼近误差的情况下,使系统跟踪误差小于预先给定的任意常数.文中用仿真算例验证了本方案的有效性.      

混合Petri网及其可达性分析

混合系统是由相互作用的离散事件动态系统和连续变量动态系统构成的复杂系统。文中建立的混合Ｐｅｔｒｉ网能够描述、分析生离散事件,以及离散事件或连续演变的并发问题,该网可以覆盖离散Ｐｅｔｒｉ网和赋时Ｐｅｔｒｉ网,从而使离散事件系统、实时离散事件和混合系统理论研究统一到同一理论框架中,此外还给出计算混合系统可达状态集的算法。     

虚拟原型技术及控制工程中的虚拟原型机

虚拟原型技术是当前设计、制造领域中的一个新技术,数字式的虚拟原型机将在很多场合替代物理原型机的使用,大大缩短设计周期,节约设计经费。在控制系统设计中,虚拟原型机可以分成３个层次,分别完成控制律的设计,控制软件的开发和控制系统的定型验证的任务。飞行控制系统虚拟原型机是建立在局域分布式仿真基础上的全数字式,并有接入实物的能力的仿真环境。为实现飞控计算机的虚拟原型机,硬件上构筑由多台计算机构成的主从结构     

Systems design of a hybrid sail pole-sitter

This paper presents the preliminary systems design of a pole-sitter. This is a spacecraft that hovers over an Earth pole, creating a platform for full hemispheric observation of the polar regions, as well as direct-link telecommunications. To provide the necessary thrust, a hybrid propulsion system combines a solar sail with a more mature solar electric propulsion (SEP) thruster. Previous work by the authors showed that the combination of the two allows lower propellant mass fractions, at the cost of increased system complexity. This paper compares the pure SEP spacecraft with the hybrid spacecraft in terms of the launch mass necessary to deliver a certain payload for a given mission duration. A mass budget is proposed, and the conditions investigated under which the hybrid sail saves on the initial spacecraft initial mass. It is found that the hybrid spacecraft with near- to mid-term sail technology has a lower initial mass than the SEP case if the mission duration is 7 years or more, with greater benefits for longer duration missions. The hybrid spacecraft with far-term sail technology outperforms the pure SEP case even for short missions.     

返回式卫星数字姿态控制系统及飞行试验结果

简要介绍我国返回式卫星上用的计算机数字姿态控制系统的方案;重点阐述姿态确定和相平面控制律的设计方法;最后简述飞行试验的结果。     

基于扩展Petri网的除冰软件安全需求建模和验证

Petri网是形式化的系统建模方法,以严格的数学基础来保证系统的正确构建,但在支持复杂软件建模和自动化验证方面存在不足.扩展了Petri网的形式语义,区别定义了状态型和数值型库所,区别定义了变迁的激发和抑制状态,引入了无前置、一元和组合判断规则,同时根据形式化定义将模型自动转换为检验程序实施安全性验证.最后给出了以上方法在典型安全关键软件-除冰系统上的应用,过程和结果表明扩展的模型和方法增强了Petri网对复杂软件系统的建模能力,提高了软件的安全性,从模型到验证代码的自动转换解决了完善模型时人工修改相应代码的工作量和因此而引入人为错误的重复工作量的问题.     

大规模设备协同中的时间建模与验证

针对大规模设备协同系统中时间属性复杂、时间约束验证困难的特点,给出了大规模设备协同中的时间属性建模方法.针对设备操作时间和状态维持时间2种时间属性,通过在操作上附加时间属性实现了对设备操作时间的建模,通过在连接符上附加时间区间属性,实现了对状态维持时间的建模.在此模型的基础上,给出了大规模设备协同中4种基本结构的时间计算方法,并通过结构等价,将基本结构等价为一个连接符,从而实现了一个设备协同模型中所有节点的时间计算;并给出了大规模设备协同中的时间约束验证规则.通过相关比较及实验分析,验证了该方法具有更高的准确度,计算偏差较低且稳定,能够满足大规模设备协同系统的性能要求.     

基于模型化配置的星务自主控制软件设计与应用

卫星互联网正成为一种空间基础设施展开建设,大规模卫星发射的需求与地面运控管理任务指数型增长之间的矛盾日益突出,特别是对于低轨长期处于测控不可见弧段运行,其自主生存需求更为急迫,而星务自主控制功能是实现自主运行和生存的重要组成.本文通过参数装订、逻辑子层和数据交互模块的架构设计,提出一种基于模型化配置的自主管理软件系统框架,并针对核心逻辑子层,建立遥控主动模型、遥测主动模型以及数据融合交互控制模型,实现星务自主管理软件的快速研制,解决自主运行功能常会随设计深入和试验验证不断功能扩展的问题,提高星务自主控制软件的灵活性.通过卫星故障检测和恢复(FDIR)自主管理功能的设计进行了验证.结果表明该软件系统设计框架能够满足星务自主控制功能设计,具备可扩展能力,为进一步提升卫星的智能化水平奠定基础.     

多机械臂的分布式自适应迭代学习控制

针对拓扑结构为无向连通的多机械臂系统,提出了一种自适应与迭代学习相结合的分布式控制协议来实现整个系统对给定期望参考轨迹的一致性跟踪.通过引入一个适当的自适应迭代学习参数,所提自适应迭代学习控制协议能够克服机械臂系统中的干扰和模型不确定性,并且每个机械臂的自适应迭代学习控制(AILC)律仅需要利用其与邻居机械臂的相对交互信息.进一步,在只有一部分机械臂具有期望参考轨迹信息的前提下,该控制协议可以实现整个系统对期望参考轨迹的跟踪,同时能够保证轨迹跟踪误差与控制输入的有界性.此外,利用李亚普诺夫分析方法证实了所得结论的正确性,并且通过一个实例验证了所提自适应迭代学习控制协议的有效性.      

敏捷性导弹的建模与模糊变结构控制

新型精确制导导弹为了获得更大的机动性、敏捷性和更高的命中精度,大多采用了推力矢量控制或反作用推力控制.讨论了敏捷性导弹的动力学特性及数学建模,并针对一类反作用推力控制的导弹提出了一种具有实时逻辑切换能力的变结构模型跟踪控制方案,为减弱一般变结构控制系统的抖颤问题,在变结构控制系统中引入简单的模糊规则,有效抑制了变结构系统的抖颤,同时进一步增强了控制系统的鲁棒性.数学仿真表明控制方案的有效性.