基于抽象解释的航空并发软件形式化验证方法研究

《基于抽象解释的航空并发软件形式化验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、2018届研究⽣硕⼠学位论⽂分类号：学校代码：10269密级：学号：51151500020EastChinaNormalUniversity硕士学位论文MASTER’SDISSERTATION论文题目：基于抽象解释的航空并发软件形式化验证方法研究院系:计算机科学与软件工程学院专业名称:软件工程研究方向:形式化方法指导教师:刘静教授学位申请人:姜庆宇2018年10⽉Dissertationformasterdegreein2018UniversityCode:10269StudentID:51151500020EASTCHINANORMA

2、LUNIVERSITYResearchonFormalVerificationofConcurrentAvionicsSoftwareBasedonAbstractInterpretationDepartment:SchoolofComputerScienceandSoftwareEngineeringMajor:SoftwareEngineeringResearchdirection:FormalMethodSupervisor:Prof.JingLiuCandidate:QingyuJiang2018.10姜庆宇硕士学位论文答辩委员

3、会成员名单姓名职称单位备注张苗苗研究员同济大学主席徐雨清高级工程师上海软件产业促进中心赵慧教授华东师范大学摘要在软件⽣命周期中，软件测试是保证软件质量的重要环节之⼀。软件测试可分为动态检测和静态检测，动态检测是通过测试⽤例在运⾏时检测正确性，静态检测则是直接分析源代码。静态检测技术通过强⼤的抽象解释使分析精确⽽⾼效，并且拥有⾃动化、完善性（完全控制和数据覆盖）等特点，使其在⼯业环境中成为⼀种⼴受欢迎的⽅法。但随着计算机技术的发展，并发软件已经有了⼴泛的应⽤。并发软件的发展给软件测试带来了新的挑战，执⾏路径的不确定性是并发软件的重要特性，

4、也是测试的难点所在，由于并发状态空间较⼤，直接将顺序程序的静态检测技术应⽤于交错执⾏的并发程序中效果并不好。线程模块化分析⽅法不⽤考虑线程交织以及相关的执⾏构建说明，可以通过分别分析每个线程来实现对并发程序的验证。线程模块化分析⽅法的主要优势在于可以⽤最⼩的代价将顺序抽象解释器提升为并发抽象解释器。该⽅法的核⼼思想分做两个步骤：⾸先，创建线程，并将所有的线程作为⼀个独⽴的顺序程序进⾏分析，同时收集其他线程对其变量的影响。然后，重新分析所有的线程，并且计算线程间的⼲涉，保存发现的新的⾏为和新的可能的⼲涉。递归这个过程直到⼲涉稳定。但传统的

5、线程模块化分析⽅法是基于线程交互的⾮关系型流不敏感的具体语义，分析更容易处理但结果不是很准确，本⽂在线程模块化分析⽅法的基础上实现了线程间的流敏感并提出了⼀种基于数据流图的约束，使分析结果更加准确。本⽂主要创新点如下：1.在原始模块化分析⽅法的基础上，我们提出了⼀种基于抽象解释的流敏感的线程模块化分析⽅法，使分析更加准确。2.我们开发了⼀种轻量级的基于数据流图的约束框架，⽤于检测线程内的⼲涉是否有效，以提⾼分析效率，提升分析精度。i3.在上述理论研究⽀持下，我们基于这种算法开发了⼀个⾯向嵌⼊式并发程序的分析⼯具原型。4.以验证航空发动机

6、控制系统为例，通过应⽤我们的线程模块化分析⽅法对系统进⾏了静态检测，展⽰了算法对嵌⼊式并发程序分析与验证的能⼒。关键词:形式化验证，抽象解释，并发程序，流敏感，约束iiABSTRACTSoftwaretestingisoneoftheimportantaspectsofsoftwarequalityassuranceduringthesoftwarelifecycle.Softwaretestingcanbedividedintodynamicdetectionandstaticdetection.Dynamicdetectionist

7、hecorrectnessofthetestcaseatruntime,whilestaticde-tectionisthedirectanalysisofthesourcecode.Staticdetectiontechnologymakesanalysisaccurateandefficientthroughpowerfulabstractinterpretation,andhasthecharacteristicsofautomation,perfection(fullcontrolanddatacoverage),makinga

8、popularmethodinindustrialenvironments.Butwiththedevelopmentofcomputertechnology,concurrentsoftwarehasbe