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

发布时间：2020-08-08 20:21

【摘要】：在软件生命周期中,软件测试是保证软件质量的重要环节之一。软件测试可分为动态检测和静态检测,动态检测是通过测试用例在运行时检测正确性,静态检测则是直接分析源代码。静态检测技术通过强大的抽象解释使分析精确而高效,并且拥有自动化、完善性(完全控制和数据覆盖)等特点,使其在工业环境中成为一种广受欢迎的方法。但随着计算机技术的发展,并发软件已经有了广泛的应用。并发软件的发展给软件测试带来了新的挑战,执行路径的不确定性是并发软件的重要特性,也是测试的难点所在,由于并发状态空间较大,直接将顺序程序的静态检测技术应用于交错执行的并发程序中效果并不好。线程模块化分析方法不用考虑线程交织以及相关的执行构建说明,可以通过分别分析每个线程来实现对并发程序的验证。线程模块化分析方法的主要优势在于可以用最小的代价将顺序抽象解释器提升为并发抽象解释器。该方法的核心思想分做两个步骤:首先,创建线程,并将所有的线程作为一个独立的顺序程序进行分析,同时收集其他线程对其变量的影响。然后,重新分析所有的线程,并且计算线程间的干涉,保存发现的新的行为和新的可能的干涉。递归这个过程直到干涉稳定。但传统的线程模块化分析方法是基于线程交互的非关系型流不敏感的具体语义,分析更容易处理但结果不是很准确,本文在线程模块化分析方法的基础上实现了线程间的流敏感并提出了一种基于数据流图的约束,使分析结果更加准确。本文主要创新点如下:1.在原始模块化分析方法的基础上,我们提出了一种基于抽象解释的流敏感的线程模块化分析方法,使分析更加准确。2.我们开发了一种轻量级的基于数据流图的约束框架,用于检测线程内的干涉是否有效,以提高分析效率,提升分析精度。3.在上述理论研究支持下,我们基于这种算法开发了一个面向嵌入式并发程序的分析工具原型。4.以验证航空发动机控制系统为例,通过应用我们的线程模块化分析方法对系统进行了静态检测,展示了算法对嵌入式并发程序分析与验证的能力。
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP311.53
【图文】：

坐标系,斜线

y) 中是否存在除零错误。1. 根据 x,y 的值建个坐标系，来表所有 x 和 y 可能的取值范围，如图2.2在第象限的斜线表 a = b 的情况，即可能会出现除零的集合。2. 如何判断变量 a,b 会同时取到斜线上的值，最简单粗暴的式是进枚举，检查所有 a,b 可能的取值，看是否同时在这条斜线上，这是种普通测试的做法。随着变量的增多，这种法的作量的增长是指数级的，所以不可能枚举出所有的可能值。利抽象解释，我们可以根据规则对程序进

取值,矩阵,矩形,交运算

图 2.2: 建坐标系图 2.3: 矩阵取值法例利区间分析的法，得到变量的最值和最值，如图2.3，在维坐标系中画个矩形，矩形框内的值是变量 x,y 所有可能的取值， xi, xa, yi, ya来分别表 x,y 的最值和最值。然后我们通过对矩形集合和斜线集合做交运算，如果运算结果为空，则说明不存在除零的可能，如果交集不为空，则说明有除零的可能。3. 上的法虽然可以解决问题，但效率很低，因为利 x 和 y 画出的矩形抽象的太粗糙，包含很多 x,y 不可能的赋值

控制流图,结构流,控制流图,赋值

抽象的太粗糙，包含很多 x,y 不可能的赋值，我们可以继续优化，将按照规则，将矩形细化，建多个精确的多边形，其中利变量 x,y 在程序中的关系，并且根据控制流图和结构流图，我们可以画出如图2.4所。10

【参考文献】