面向altarica模型的系统安全性设计验证方法研究

《面向altarica模型的系统安全性设计验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP311论文编号：102871616-S055学科分类号：083500硕士学位论文面向AltaRica模型的系统安全性设计验证方法研究研究生姓名仵志鹏学科、专业软件工程研究方向软件安全性分析与验证指导教师王珊珊副教授南京航空航天大学研究生院计算机科学与技术学院二〇一六年三月NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyResearchonVerificationMethodologyaboutSystemSafe

2、tyDesignBasedonAltaRicaModelAThesisinSoftwareEngineeringbyWuZhipengAdvisedbyAssociateProf.WangShanshanSubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofMasterofEngineeringMarch,2016南京航空航天大学硕士学位论文摘要随着计算机技术的迅速发展，嵌入式系统在医疗、交通、通信、航空航天等安全关键领域已得到广泛运用。如何提高系统的安全性，防止灾难性事故发生，已经成为当前软件工程领域重要的研

3、究课题。AltaRica语言是一种描述正常情况下系统功能行为，同时描述系统存在的失效行为的建模语言，面向AltaRica模型的系统安全性分析是当前的研究热点之一。目前已有相应的一些工具利用AltaRica模型进行系统安全性分析，而支持AltaRica模型的穷举分析和时序属性方面的验证工具还很缺少，成熟的模型检测工具SPIN对模型的穷举分析和线性时序逻辑验证有很大优势，但SPIN工具并不能直接对AltaRica模型进行验证。针对以上问题，本文首先将AltaRica模型转换到Promela模型，对安全需求使用线性时序逻辑进行规约；然后将Promela模型导入模型检测工具SPIN进

4、行验证和分析；最后结合验证结果和可追踪性信息模型，追踪AltaRica模型存在的设计缺陷。本文的主要研究内容如下：第一，通过对AltaRica模型和Promela模型的语义分析，提出了AltaRica模型到Promela模型的转换规则，并对两模型语义的等价性进行证明。使用线性时序逻辑对安全性需求进行规约并结合转换得到的Promela模型导入模型检测工具进行形式化验证。在此基础上，提出一种面向AltaRica模型的系统安全性设计验证方法。第二，针对模型检测的验证结果，给出了根据验证结果的反例路径追踪到AltaRica模型设计缺陷的可追踪性信息模型。通过对验证结果和AltaRic

5、a模型的分析，首先给出验证结果可追踪性信息模型的元模型；然后根据具体的追踪目标实例化元模型，得到可追踪性信息模型；最后基于可追踪性信息模型设计追踪算法，实现根据验证结果的反例路径追踪查找AltaRica模型的设计缺陷甚至系统组件存在的安全性问题。第三，针对本文提出的面向AltaRica模型的系统安全性设计验证方法，设计并实现相应的原型工具A2STool，对A2STool的功能模块进行相应地说明，并给出该工具的设计框架、执行流程以及关键的实现技术。最后，运用本文提出的方法对机轮刹车系统控制单元进行案例分析，利用原型工具给出了AltaRica模型到Promela模型转换的完整过程

6、，使用SPIN对Promela模型和安全性需求的线性时序逻辑规约进行验证和分析，接着基于验证结果结合可追踪性信息模型发现系统安全性设计缺陷。说明了本文方法的有效性和可行性，为系统的安全性分析提供了一种新思路。关键词：系统安全性设计，AltaRica模型，线性时序逻辑，可追踪性信息模型，模型检测I面向AltaRica模型的系统安全性设计验证方法研究ABSTRACTWiththerapiddevelopmentofcomputertechnology,embeddedsystemhasbeenwidelyusedinthesafetycriticalfieldsuchasmedi

7、caltreatment,transportationcommunication,aeronauticandastronautics.Howtoimprovesystemsafetyandpreventcatastrophicaccidenthasbeenanhottopicinthefieldofsoftwareengineering.AltaRicaisakindofmodelinglanguage,whichdescribesthebehaviorofasysteminanormalcaseand