面向测试和模型检测需求的程序建模技术研究

1绪论

1.1研究现状

对被测统建模是软件测试和模型检测的关键需求，目前程序建模方法和过程仍然是一个具有挑战性的难题。目前模型检测的研宄中，以程序控制流图为分析对象的流分析是重要的模型检查方法。文献是在程序的源代码层面采用基于程序控制流提取的模型检查方法，基于扩展的程序流图生成抽象有限现实模型，并利用模型检查算法验证有限现实模型性质的正确性。文献采用的是抽象现实机模型ASM是模型检测的基础；然而当源程序复杂到一定程度，模型的复杂度也会增加，建模过程很难保证一致性，提出方法与技术的适用程度有待于进一步扩展。文献和分别采用的工具为SPIN和BLAST，采用的建模方法和技术强烈地依赖具体建模工具，而这些工具的建模能力缺乏等价性的证明。综上所述，目前对程序建模主要是基于程序的源代码，并且很难保证建模过程的一致性。

程序流图是程序的控制流转路径的径静态抽象表示，它是程序中所有可能的执行路径集合，在静态检测、程序测试以及程序分析和理解中有着广泛的应用虽然程序流图自动生成的相关研究已经比较成熟稳重，但还不够完善。文献从源代码分析出发，构建抽象语法树分析出包含在if,while,switch等句子中的控制流，从源代码程序中提炼出程序控制流图的算法。文献提出的程序流图自动生成算法，没有根据基本块自动划分节点，而是规定节点ID为代码所在行的号码，应用中有一定的局限性，但文献对主要的句子控制结构进行了深入的分析和研究，并设计开发了程序控制流图生成工具。文献构造的控制流图只能能反映一个过程的实时执行过程，不能有效处理过程间的控制流关系。文献研究生成的控制流图是基于java语言的程序，利用Eclipse环境开发出相应的插件对程序流图进行可视化输出。

1.2课题研究内容和方法

本文针对测试和模型检测需求提出了一种程序建模技术，该技术主要包括物理存储模型，可视化模型和代数模型。利用程序流图的思想建立物理存储模型和可视化模型，并通过建立在严格数学基础上的代数模型验证可视化模型的正确性。本课题主要集中于支持测试和模型检测需求的应用研究和建模工具研究，利用程序流图的思想进行建模的核心内容包括：

1）根据基本块划分想自动划分PDL-C描述的被测系统，构造节点实现系统级别的构造，并且完成构造节点的算法研究。

2）通过研究文献对面向服务体系结构SOA形式化和可信属性建模研究的基础上进行应用和扩展。完成程序流图到软件体系结构代数模型的概念映射和程序流图到服务组合运算的映射研究。

3）在映射规则的基础上，利用把一个基本的服务组合运算继续抽象成一个服务组件进行组合运算的思想，最终实现用一个代数式描述整个程序流图，生成代数模型。完成PDL-C描述的被测系统到程序代数模型转换的算法研究，并利用代数模型证明生成的程序流图的正确性。

4）根据以上算法，设计实现程序建模工具。

2相关理论和技术介绍

以下就本文涉及的相关理论和技术做简要介绍。包括基本路径测试方法，WEB服务描述语WSDL言和服务组合描述语言BPEL。

2.1基本路径测试法

基本路径不仅可以帮助软件测试，同时本课题还利用基本路径测试方法支持模型检测，一定程度上解决空间爆炸的问题。基本路径的构成思路：基本路径测试方法的研究是在程序控制流图的基础上的，通过分析控制流图的环路复杂性，算出基本路径集合，根据基本路径设计测试用例。在基本路径测试中，要保证每条句子至少执行一次，即每条单独的基本路径中都要包括一个与其他路径不同的节点。并且在基本路径测试方法中，需要对程序流图进行可视化的输出。

首先利用基本的流图符号画出程序的流图，基本的流图符号如图2.1所示：

环路复杂度是用来度量程序逻辑复杂性的，改度量用来计算程序的基本路径数目，测量上界就是所有句子至少执行一次，每条独立路径都包含一条未曾用过的边。三种方法计算环路复杂度。计算流图中区域的数量，或利用流图中边的数量减去流图中节点的数量加二，或利用判定节点的数量加一。

基本路径法步骤：

步骤1:以源代码或者详细设计文档为基础，绘制出相应的程序流图。

步骤2:计算程序流图的环路复杂度。

步骤3:确定线性无关的基本集。

步骤4:设计测试用例，确保执行基本集中每条路径。

2.2WEB服务概述

物理存储模型中采用WSDL/BPEL的部分定义和规则对程序流图进行描述和存储，支持后续的模型检测和软件测试。以下对WSDL/BPEL的相关知识进行介绍。

3程序建模基础研究........8

3.1子程序划分..........8

3.2基本块划分.........9

4程序建模体系研究........12

4.1代数模型表述.........12

5程序建模工具的设计与实现........26

5.1程序建模工具的设计...............26

6案例分析

6.1八皇后算法建模

八皇后问题是一个以国际象棋为背景的问题：在8*8的国际象棋棋盘上放置八个皇后，为了使得任何一个皇后都无法直接吃掉其他的皇后，任两个皇后都不能处于同一条横行、纵行或斜线上。本文用到的八皇后算法伪代码程序包括四个函数，分别是主函数main、查找函数search、判断函数judge、结果输出函数showAnswer。以下为Model System工具的具体使用。

结论

本文应用程序流图的思想对程序建模，满足了测试和模型检测的需求。文献是直接分析程序的源代码构造扩展程序控制流图，本文提出的程序建模技术是分析程序的PDL-C伪代码生成控制流，用伪代码描述程序处于软件工程中的设计阶段，先于源代码的生成阶段，因此可以更早的检测出程序的错误和缺陷。当源程序复杂到一定程度，模型的复杂度也会增加，建模过程很难保证一致性。针对此问题，本文提出了同时支持模型检测和软件测试的建模技术，并利用提出的程序代数模型对生成的可视化模型进行正确性的验证，保证了所建模型的可靠性和一致性。文献提出的程序流图自动生成算法，节点ID规定为代码所在行的号码，应用中有一定的局限性。本文根据基本块自动划分，更灵活，自动化程度更高。文献构造的控制流图只能能反映一个过程的实时执行过程，不能有效处理过程间的控制流关系。本文对整体程序根据函数进行模块划分可以实现程序间的控制流关系，有效的描述了整个被测系统。

参考文献（略）