基于时序故障树的实时系统安全性验证方法研究

《基于时序故障树的实时系统安全性验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP311论文编号：102871616-SZ024学科分类号：085212硕士学位论文基于时序故障树的实时系统安全性验证方法研究研究生姓名王思琪专业类别工程硕士专业领域软件分析与验证指导教师黄志球教授南京航空航天大学研究生院计算机科学与技术学院二〇一六年一月NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyResearchonReal-timeSystemsSafetyV

2、erificationBasedonTemporalFaultTreeAThesisinSoftwareAnalysisandVerificationbyWangSiqiAdvisedbyProf.HuangZhiqiuSubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofMasterofEngineeringJanuary,2016承诺书南京航空航天大学全日制专业硕士学位论文摘要伴随实时系统在信息关键领域的广泛应用，其复杂度也在不断增加，如何保证实时系统安全性，

3、避免财产损失甚至人员伤亡等灾难性事故的发生，已成为当前软件工程领域的研究重点。目前针对软件安全性分析的研究工作主要集中在软件需求规约和功能设计阶段，以故障分析及功能建模方法作为主要技术支持。然而在软件的实际开发过程中，安全需求分析和软件设计过程相对独立，研究工作尚未统一，致使一方面安全需求分析结果难以应用于软件设计之中为其提供指导；另一方面设计模型中缺乏安全属性来源无法对系统安全性予以保障。传统的故障树分析法及其扩展模型可用于安全需求获取，但无法确定获取的安全需求在系统设计中是否得到满足。系统体系结构分析与设计语言AADL能够对

4、系统功能及非功能属性进行描述，但缺乏对系统安全需求的直观表达，很难发现系统的潜在危害。本文利用模型检测技术，将安全需求分析与软件功能设计相结合，提出一种基于扩展故障树的实时系统安全性验证方法。该方法通过验证时序故障树中提取的安全属性是否在AADL建立的系统模型中得到满足实现系统安全性验证工作。论文主要研究内容如下：（1）为解决实时系统安全性验证问题，提出一种结合时序故障树提取的安全属性与AADL建立的系统模型对软件安全性进行验证的分析框架。（2）为保证最小割集求解的软件安全属性的正确性，采用分步确认的方法，为验证工作的正确执行提

5、供保障。主要包括结合测试用例的方法对时序故障树的构建正确性进行验证以及借鉴定理证明的思想对安全属性规约进行一致性检测。（3）为提供安全属性验证所需系统模型，给出AADL建模子集到时间自动机的转换规则，实现AADL模型到时间自动机模型的自动转换，在模型检测工具UPPAAL下对安全属性进行验证和分析。最后，将本文提出的方法运用到汽艇自动驾驶系统的案例分析中，给出系统时序故障树的构建及约简过程，验证了时序故障树构建的正确性及提取的安全属性的一致性；同时，给出系统速度控制模块的AADL建模，将AADL模型转换为时间自动机网，用UPPAA

6、L进行了验证与分析，发现系统设计缺陷，以此说明了本文方法的可行性和有效性，为嵌入式软件的安全性分析工作提供了一种新思路。关键词：故障树分析，时序故障树，AADL，时间自动机，模型检测I基于时序故障树的实时系统安全性验证方法研究ABSTRACTThecomplexityofreal-timesystemsisincreasingtogetherwithitsrapiddevelopmentincriticalinformationarears,tosolvetheproblemofhowcanweguaranteethesafet

7、yofreal-timesystems,keepthemawayfromaccidenthasbecometheemphasisinsoftwareengineeringresearch.Nowadays,researchonsoftwaresafetyanalysismainlyfocusonrequirementsspecificationandsoftwarefunctionaldesignsupportedbyfaulttreeanalysisandfunctionalmodeling.Howeverthetwoares

8、eparatedinsoftwaredevelopment,whichmakesthatontheonehand,analysisresultfromsafetyrequirementscanbehardlyreflectedtosoftwaredesignfo