摘要
摘要
无人机飞行控制系统作为飞行器关键系统之一，负责飞行器从起飞至降落的整个飞行过程。飞控系统软件具有安全性能要求高、功能繁多、复杂性高的特点，而传统的软件开发方式存在诸多不足。同时采用形式化验证方法对飞控系统软件进行安全性验证时，安全属性的提取没有统一的有效的方法；安全属性的验证过中易产生空间爆炸问题，研究如何对状态空间进行约简也是当前所的面临的重要任务。 本文采用了基于模型的软件开发工具SCADE开发飞控系统软件，同时针对飞控系统软件高安全可靠性的要求，研究了基于故障树的安全属性提取方法，并结合模型检验技术，进行安全性验证。针对验证过程中产生空间爆炸问题，提出了基于切片和系统分解的方法对验证空间进行划分，分步验证。本文主要包括以下内容： 首先对安全属性提取方法及模型检验技术进行研究。介绍了基于模型的软件开发方式，给出了故障树的构建准则和安全属性提取及转化方法。然后，对状态空间约简问题进行研究。针对形式化验证过程中出现的状态空间爆炸问题，采用了基于切片和系统分解的方法对状态空间进行约简。最后进行飞控系统建模及典型模块形式化验证。对飞控系统软件进行需求分析、功能模块划分并建模，并针对典型模块进行安全属性提取及形式化验证。然后由模型自动生成代码，并在虚拟仿真测试平台上测试验证了其功能和 性能，并与手工代码进行运行时间对比。
本文的研究对飞控系统软件基于模型的软件开发、安全属性提取、状态空间约简及形式化验证工作有一定的促进作用，为其他基于模型的开发和验证工作提供了一定的帮助。
关键词：飞控系统建模，安全属性提取，形式化验证，状态空间约简
ABSTRACT
UA V flight control system as one of the key aircraft system is responsible for the entire flight process of the aircraft from taking-off to landing. The flight control system software has the characteristics of safety-critical performance, multifunction and high complexity. However there are many deficiencies in traditional software development methods. At the same time, the formal verification method is used to verify the safety of the flight control system software. There is no unified and effective method to extract the safety properties. The validation of the safety properties is prone to the space explosion problem. How to reduce the state space is also an important task in the current situation.
In this thesis, the software development tool SCADE is used to develop the flight control system software. At the same time, the safety property extraction method based on the fault tree is studied i
n view of the safety-critical and reliability requirements of the flight control system software. The safety verification is carried out in combination with the model checking. In order to solve the space explosion in the process of verification, this thesis proposes a method of segmenting and verifying the verification space based on the slicing and system decomposition. This thesis mainly includes the following aspects:
Firstly, we study safety property extraction method and model checking technique. This thesis introduces the model of software development based on model, and puts forward the construction criteria of specific fault tree and the method of safety property extraction and transformation. Secondly，the problem of state space reduction is studied. In order to solve the problem of state space explosion during formal verification, the state space is reduced by using slicing and system decomposition methods. Finally, we carry out flight control system modeling and formal verification of typical modules. We analyze the requirements of the flight control system software, divide and model functional modules. The safety properties are extracted and verified for the typical modules. The code generated from the models is loaded into the emulation testing platform to verify its functionality and performance, and compares it with the manual code.
The research of this thesis has a certain effect on the software development, safety
property extraction, state space reduction and formal verification of flight control system software, which provides some help for other model-based development and verification workers.
Keywords: flight control system modeling, safety property extraction, formal verification, state space reduction
目录
第一章绪论 (1)
1.1研究背景 (1)
1.2国内外研究现状 (2)
1.2.1基于模型的软件开发方法 (2)
1.2.2故障树分析法研究现状 (3)
1.2.3模型检验技术研究现状 (3)
1.3主要研究内容 (5)循环水旁滤过滤器
1.4论文的组织结构 (5)
第二章故障树分析法及模型检验 (6)
2.1故障树分析法 (6)
2.1.1故障树的构建 (6)
无动力滑翔伞2.1.2故障树的规范化及约简 (7)
2.1.3故障树定性分析 (8)
2.2模型检验 (9)
2.2.1形式化验证技术 (9)
2.2.2状态转移系统 (10)
2.2.3基于可满足性的模型检验 (11)
2.2.4可满足性公式 (12)
分集接收
2.3故障树分析法与模型检验相结合 (14)
2.4本章小结 (16)
第三章安全属性提取方法及状态空间约简研究 (17)
3.1安全属性提取方法 (17)
3.1.1构建准则 (17)
3.1.2安全属性提取 (18)
3.2验证策略研究 (20)
3.2.1模块化验证 (20)
3.2.2Design Verifier验证策略 (20)
3.2.3非回归性证明和降阶模型分析 (21)
3.3状态空间约简 (21)
3.3.1系统模型切片 (22)
3.3.2验证属性切片 (22)
3.3.3条件切片 (22)
3.3.4操作符内部处理 (23)
3.4本章小结 (23)
第四章飞控系统建模及测试验证 (24)
4.1状态监控和余度管理模块设计与实现 (26)
4.2导航和大气子系统监控管理模块设计与实现 (27)
4.3交联系统状态监控管理模块设计与实现 (36)
4.4作动器监控管理模块设计与实现 (40)
4.5飞行控制模块设计与实现 (41)
4.6姿态解算模块设计与实现 (43)
4.7高度控制模块设计与实现 (45)
msinfo4.8遥控模块设计与实现 (46)
4.9测试验证 (47)
4.9.1模拟测试 (47)
4.9.2测试用例设计 (49)
4.9.3测试执行 (49)
4.9.4覆盖率分析 (50)
4.9.5测试结果分析 (51)
4.10本章小结 (52)
第五章飞控系统典型模块形式化验证 (53)
pst1685.1着陆架监控管理模块形式化验证 (53)
医用护理床
5.1.1着陆架监控管理模块故障树构建 (53)
5.1.2着陆架监控管理模块安全属性提取 (54)
5.1.3着陆架监控管理模块安全属性建模及形式化验证 (55)
5.2姿态控制模块形式化验证 (57)
5.2.1姿态控制模块故障树构建 (58)
5.2.2姿态控制模块安全属性提取 (59)
5.2.3姿态控制模块安全属性建模及形式化验证 (60)
5.3闭环仿真 (62)
5.3.1虚拟飞行控制仿真平台 (62)
5.3.2闭环仿真 (63)
5.3.3运行时间对比 (65)
豫公网安备41160202000603
站长QQ:729038198
关于我们
投诉建议