基于模型检验的EFVS安全性建模与分析技术研究

发布时间：2025-01-15 12:00

　　增强飞行视景系统作为飞机上的复杂电子系统,传统的安全性分析面临工作量大,过于依赖分析人员经验,容易出错等问题,Petri网、概率模型等形式化方法虽然提高了分析的自动化水平,减少了一定的分析工作量,但也面临不能自上而下进行安全性需求分配的问题。为解决上述问题,提出了基于模型检验的形式化安全性分析方法。实现对增强飞行视景系统的定性、定量安全性分析,提高分析效率。研究包括以下几个方面:(1)首先,通过对该系统的架构和数据流进行抽象,分模块级、LRU级、系统级三层,建立了系统的形式化名义模型,并进行了验证。(2)研究模型扩展方法,编写故障库模板,将底层模块的故障模式注入到名义模型,建立形式化扩展模型。(3)将典型失效状态用形式化规约描述,进行自动计算,得到故障树最小割集,基于该最小割集进行了定性和定量分析,其中在定量分析,提出一种安全性分配方法,并实现了自动分配工具。结果表明,该方法自动化程度高,且解决了其它形式化方法如Petri网、概率模型等无法进行自上而下概率分配的问题,能够更加有效地促进系统设计阶段的安全性工作。

【文章页数】：97 页

【学位级别】：硕士

【部分图文】：

图2-4模型检验示意

中国民航大学硕士学位论文12图2-4模型检验示意模型检验中的系统模型用Kripke结构表示。其由一个五元组MS,S0,AP,R,L=构成，其中S表示有限状态集合，0S是初始状态集合，且0S是S的子集，AP表示由原子命题及和它们的非构成的集合，R表示状态转移关系，映射L:S→2|A....

图3-1低能见度情况下飞行员裸眼

中国民航大学硕士学位论文16第三章EFVS系统形式化名义模型建模3.1建模范围模型是对事物的抽象，用严谨的语言来定义，模型是要素与要素之间联系的集合。因此在不同的情境中，模型的含意有所不同。比如，玻璃柜台中摆放的静态飞机模型，和航空爱好者制作的可以飞行的航模。二者都是模型，却有很....

图3-7非均匀校正模块RSML-e模型

中国民航大学硕士学位论文23图3-7非均匀校正模块RSML-e模型RSML-e模型的上半部分是数据定义，Image_NUCM_out表示非均匀校正模块输出的图像数据；Type表示数据类型为枚举型，有normal，error，empty三个枚举值，分别代表正常、....

图3-8非均匀校正模块状态转移条件AND-OR表

中国民航大学硕士学位论文24(（Im__）)(（__）)(（__）)ageDMouterrorTRUETRUETRUEBFDtoEVSemptyTRUETRUETRUEBFDtoEVSerror===化简的表达式为（Im....

本文编号：4027363