基于形式化模型的系统安全性分析与验证方法研究

《基于形式化模型的系统安全性分析与验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP391论文编号：102871618-SZ008学科分类号：085211硕士学位论文基于形式化模型的系统安全性分析与验证方法研究研究生姓名王明明专业类别工程硕士专业领域计算机技术指导教师胡军副教授南京航空航天大学研究生院计算机科学与技术学院二О一八年三月NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyResearchonSystemSafetyAnalysisandVerificationBased

2、onFormalModelAThesisinComputerScienceandTechnologybyWangMingmingAdvisedbyProf.HuJunSubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofMasterofEngineeringDecember,2017承诺书本人声明所呈交的硕士学位论文是本人在导师指导下进行的研究工作及取得的研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得南京航空航天大学或其他教育机构的学位

3、或证书而使用过的材料。本人授权南京航空航天大学可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。（保密的学位论文在解密后适用本承诺书）作者签名：日期：南京航空航天大学全日制专业硕士学位论文摘要随着社会的发展，安全关键性系统的使用得到了极大的发展，在安全关键性系统领域，如航空航天，核电站，高铁等，如何提高其安全性，防止出现人员伤亡和自然资源的破坏，是一个重要的研究内容。安全关键性系统（如，航电系统）的设计与分析不仅要保证系统能正常完成指定的功能，同时要保证在系统中某些部件失效时或者由于环境或人为原因导致出

4、现危险情况时，系统应该给予相应的安全性保护。首先安全关键性系统的需求规约是非常重要的，完整的明确的需求可以有效的指导系统的开发与实现。另外，安全关键性系统的开发不仅要考虑其功能性需求，对其组件可能发生的故障行为同时要给予重视。针对上述问题，本文的主要工作是设计一套可以是明确安全关键性系统需求并且可以对其故障行为进行建模并验证的方法框架，具体工作如下：(1)本文首先根据安全关键性系统需求规约的重要性，介绍了RSML-e语言对于系统需求规约的作用，RSML-e语言是一种基于四变量模型的形式化建模语言，其所建模型可以有助于系统开发者和非开发人员之间沟通需求关系。但是

5、由于RSML-e语言不具有进行模型检验的特点，本文在详细分析了RSML-e语言和NuSMV语言的语法特征之后，提出了一套将RSML-e语言转化为NuSMV语言的转化规则。基于此系统需求规约、模型转化和模型检验的思想，本文提出了一套基于NuSMV模型检验的初步需求验证框架。(2)对于安全关键性系统来说，保证功能行为的正确性只是安全性分析的第一步，进一步需要做的是对系统的故障行为进行分析。在对MBSA的方法思想和故障注入机制进行介绍之后，紧接着本文结合故障扩展和MBSA分析验证的思想提出了一种基于MBSA的系统验证与安全性分析框架，用于对功能明确的NuSMV功能模

6、型进行故障注入扩展，并对其扩展模型进行安全性评估，生成故障树和FMEA表。(3)本文以一个真实的航电系统的自动飞行系统为实例来分析，介绍了其系统架构，然后选取合适的子系统（AFCS系统）进行RSML-e需求建模，并进行模型转化到NuSMV模型，对其NuSMV模型做模型检验。例证了本文提出的基于NuSMV模型检验的初步需求验证框架的有效性和实用性。然后对该模型进行故障注入，并且在故障注入的过程中根据AFCS系统的特点，自定义了输出紊乱故障模式，成功生成了扩展模型，基于该扩展模型，使用xSAP工具自动生成了故障树和FMEA表。关键词：安全关键性系统，RSML-e，

7、模型检验，故障扩展，MBSA，故障树分析，FMEAi基于形式化模型的系统安全性分析与验证方法研究ABSTRACTWiththedevelopmentofsociety,theuseofsafety-criticalsystemshasbeengreatlyimproved.Itisanimportantresearchcontentinsafety-criticalsystemssuchasaerospace,nuclearpowerplants,andhigh-speedrailways,thathowtoimprovetheirsafetyandpreve

8、nthumancasualtiesan