机载安全关键软件模型验证技术研究
发布时间：2021-09-05 22:12
现代电子机载系统正由电子机械密集型向软件密集型转变,系统功能的实现越来越依赖于软件,导致软件的安全性对系统的安全至关重要。软件测试是开发过程中用来验证软件功能正确性的方法。然而,软件功能的正确性不能保证安全关键系统的安全运行。软件必须根据安全分析确定的安全需求进行验证并且需要识别出预期以外的功能,以确保识别出的潜在危险行为不会发生。软件的复杂性使得用传统的安全性分析方法定义适当的软件安全性需求变得困难。系统理论过程分析（System Theoretic Process Analysis,STPA）是一种基于系统理论事故模型和过程（Systems Theoretic Accident Model and Processes,STAMP）的安全性分析方法,用于识别系统危害,包括与软件相关的危害,但是该方法严重依赖分析人员经验。此外,目前在实际工程中采用基于模型的软件开发方式成为趋势。为此,本文以模型为核心,提出一种基于形式化扩展STPA方法和RTCA DO-331适航标准相结合的机载软件模型验证方法。本文的主要研究工作及创新点如下:（1）本文首先采用安全关键应用开发环境（Safety Cr...
【文章来源】：中国民航大学天津市
【文章页数】：94 页
【学位级别】：硕士
【部分图文】：
起落架控制器软件模型功能测试结果
中国民航大学硕士学位论文65经分析得到了可能导致UCA18发生的危险路径RUCA18.4，实现对危险行为的原因进行定位，可以减少人为分析的工作量。定位后只需分析已给出的导致违反SSR18.4的路径，反例的仿真结果如图4-10(c)所示，反例总共给出了15个周期的交互场景，在第13个周期时，Res4输出为false，说明此时软件中存在违反SSR18.4的危险行为，此时关键变量取值为flighttake_off,handledown,extend_EVopen,stateanormaly,对比RUCA18.4可知extend_EV信号出现错误，有可能导致当飞机处于起飞状态并且飞机未离开地面时，起落架异常解锁，导致事故发生。该系统级事故发生是由于提供extend_EV信号导致的，而该信号是在一个交互场景中被异常提供，在进行模拟仿真时很难被发现，通过本文提供的系统安全性分析方法获取的安全性需求，结合模型检验技术识别出了潜在的致因场景导致软件危险行为的发生。图4-10形式化验证结果基于已经识别出来的危险行为，通过对设计模型进行修改，消除软件中的潜在危险行为，并重新进行形式化验证识别潜在危险行为。SCADE工具中针对形式化验证结果自动生成验证报告，报告中以“valid”和“falsifiable”分别表示验证通过和不通过。在主机上执行了4s的时间之后，验证结果显示“valid”，如图4-10所示。表明软件模型通过了形式化验证，软件中不存在违反STPA分析结果的执行路径。因此可以通过形式化扩展STPA方法结合模型检验技术有效识别出软件中的危险行为，并一定程度上提升了
中国民航大学硕士学位论文71图5-2模型测试结果图5-3模型测试结果报告通过基于需求进行模型测试并生成测试结果报告表明软件完备实现了预期的功能且测试结果是正确的。但是需要进一步验证软件中是否存在预期功能以外的功能。需要对软件模型进行模型覆盖分析，通过模型覆盖分析检测软件是否执行了预期以外的功能。首先在SCADE工具中设置为MTC模式，并在MTC中设置为MC/DC覆盖准则，执行覆盖分析，最终覆盖分析结果如图5-4所示，并生成模型覆盖报告如图5-5所示。模型覆盖结果表明：最终需求实现了对软件模型的完全覆盖，即模型中不存在预期以外的功能。在此过程中本文已对根据覆盖分析结果对软件进行修改，消除了软件中非预期的分支路径。同时对生成的代码进行覆盖分析，完成对软件代码的覆盖分析，如图5-6所示。SR1.1SR1.2SR1.3SR1.4测试总结：通过
【参考文献】：
期刊论文
[1]基于STPA-Bayes模型的机载平视显示系统安全性分析与评价[J]. 赵长啸,李浩,董磊,王鹏. 系统工程与电子技术. 2020(05)
[2]基于STPA的安全分析方法在下一代列车运行控制系统中的应用[J]. 孙超. 铁路计算机应用. 2019(11)
[3]基于SCADE联锁逻辑实现与仿真分析[J]. 赵璐,张娜敏. 现代城市轨道交通. 2019(06)
[4]同步数据流语言可信编译器的研究进展[J]. 杨萍,王生原. 计算机科学. 2019(05)
[5]波音737-8事故简析[J]. 馮建文,孫黎,劉金龍. 航空动力. 2019(02)
[6]基于SCADE的列控系统车载ATP软件建模研究[J]. 王锡奎,田建兆,王若昆,张菊. 高速铁路技术. 2019(01)
[7]基于模型的核电站操作员支持系统开发与测试[J]. 侯东,黄俊,王文全,沈轶烨. 上海交通大学学报. 2018(S1)
[8]核电厂数字化仪控系统算法软件自动化生成方法[J]. 黄俊,李晓龙,赵洋,吴延群. 上海交通大学学报. 2018(S1)
[9]Safety analysis of wheel brake system based on STAMP/STPA and Monte Carlo simulation[J]. HU Jianbo,ZHENG Lei,XU Shukui. Journal of Systems Engineering and Electronics. 2018(06)
[10]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
硕士论文
[1]基于模型的无人机飞控系统建模及安全性验证方法研究[D]. 张品飞.电子科技大学 2017
[2]固定翼飞机飞行动力学及振动特性仿真研究[D]. 宁雷.哈尔滨工程大学 2016
[3]某型固定翼无人机飞控系统的设计与仿真[D]. 孔德胜.北京理工大学 2015
[4]基于模型的安全关键软件全覆盖测试方法的研究与实现[D]. 马金梭.上海交通大学 2011
[5]SCADE在无人机飞行控制软件设计中的应用[D]. 程黎.西安电子科技大学 2011
[6]基于SCADE的无人机飞行控制软件设计[D]. 颜雯清.南京航空航天大学 2008
本文编号：3386179
【文章来源】：中国民航大学天津市
【文章页数】：94 页
【学位级别】：硕士
【部分图文】：
起落架控制器软件模型功能测试结果
中国民航大学硕士学位论文65经分析得到了可能导致UCA18发生的危险路径RUCA18.4，实现对危险行为的原因进行定位，可以减少人为分析的工作量。定位后只需分析已给出的导致违反SSR18.4的路径，反例的仿真结果如图4-10(c)所示，反例总共给出了15个周期的交互场景，在第13个周期时，Res4输出为false，说明此时软件中存在违反SSR18.4的危险行为，此时关键变量取值为flighttake_off,handledown,extend_EVopen,stateanormaly,对比RUCA18.4可知extend_EV信号出现错误，有可能导致当飞机处于起飞状态并且飞机未离开地面时，起落架异常解锁，导致事故发生。该系统级事故发生是由于提供extend_EV信号导致的，而该信号是在一个交互场景中被异常提供，在进行模拟仿真时很难被发现，通过本文提供的系统安全性分析方法获取的安全性需求，结合模型检验技术识别出了潜在的致因场景导致软件危险行为的发生。图4-10形式化验证结果基于已经识别出来的危险行为，通过对设计模型进行修改，消除软件中的潜在危险行为，并重新进行形式化验证识别潜在危险行为。SCADE工具中针对形式化验证结果自动生成验证报告，报告中以“valid”和“falsifiable”分别表示验证通过和不通过。在主机上执行了4s的时间之后，验证结果显示“valid”，如图4-10所示。表明软件模型通过了形式化验证，软件中不存在违反STPA分析结果的执行路径。因此可以通过形式化扩展STPA方法结合模型检验技术有效识别出软件中的危险行为，并一定程度上提升了
中国民航大学硕士学位论文71图5-2模型测试结果图5-3模型测试结果报告通过基于需求进行模型测试并生成测试结果报告表明软件完备实现了预期的功能且测试结果是正确的。但是需要进一步验证软件中是否存在预期功能以外的功能。需要对软件模型进行模型覆盖分析，通过模型覆盖分析检测软件是否执行了预期以外的功能。首先在SCADE工具中设置为MTC模式，并在MTC中设置为MC/DC覆盖准则，执行覆盖分析，最终覆盖分析结果如图5-4所示，并生成模型覆盖报告如图5-5所示。模型覆盖结果表明：最终需求实现了对软件模型的完全覆盖，即模型中不存在预期以外的功能。在此过程中本文已对根据覆盖分析结果对软件进行修改，消除了软件中非预期的分支路径。同时对生成的代码进行覆盖分析，完成对软件代码的覆盖分析，如图5-6所示。SR1.1SR1.2SR1.3SR1.4测试总结：通过
【参考文献】：
期刊论文
[1]基于STPA-Bayes模型的机载平视显示系统安全性分析与评价[J]. 赵长啸,李浩,董磊,王鹏. 系统工程与电子技术. 2020(05)
[2]基于STPA的安全分析方法在下一代列车运行控制系统中的应用[J]. 孙超. 铁路计算机应用. 2019(11)
[3]基于SCADE联锁逻辑实现与仿真分析[J]. 赵璐,张娜敏. 现代城市轨道交通. 2019(06)
[4]同步数据流语言可信编译器的研究进展[J]. 杨萍,王生原. 计算机科学. 2019(05)
[5]波音737-8事故简析[J]. 馮建文,孫黎,劉金龍. 航空动力. 2019(02)
[6]基于SCADE的列控系统车载ATP软件建模研究[J]. 王锡奎,田建兆,王若昆,张菊. 高速铁路技术. 2019(01)
[7]基于模型的核电站操作员支持系统开发与测试[J]. 侯东,黄俊,王文全,沈轶烨. 上海交通大学学报. 2018(S1)
[8]核电厂数字化仪控系统算法软件自动化生成方法[J]. 黄俊,李晓龙,赵洋,吴延群. 上海交通大学学报. 2018(S1)
[9]Safety analysis of wheel brake system based on STAMP/STPA and Monte Carlo simulation[J]. HU Jianbo,ZHENG Lei,XU Shukui. Journal of Systems Engineering and Electronics. 2018(06)
[10]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明. 软件学报. 2019(01)
硕士论文
[1]基于模型的无人机飞控系统建模及安全性验证方法研究[D]. 张品飞.电子科技大学 2017
[2]固定翼飞机飞行动力学及振动特性仿真研究[D]. 宁雷.哈尔滨工程大学 2016
[3]某型固定翼无人机飞控系统的设计与仿真[D]. 孔德胜.北京理工大学 2015
[4]基于模型的安全关键软件全覆盖测试方法的研究与实现[D]. 马金梭.上海交通大学 2011
[5]SCADE在无人机飞行控制软件设计中的应用[D]. 程黎.西安电子科技大学 2011
[6]基于SCADE的无人机飞行控制软件设计[D]. 颜雯清.南京航空航天大学 2008
本文编号：3386179
本文链接：https://www.wllwen.com/shoufeilunwen/xixikjs/3386179.html
