基于形式化规约的缺陷规则库构建与检测方法

佟超，王建新，齐建东

北京林业大学信息学院，北京100083

1 引言

程序缺陷分析是软件质量保证的重要组成部分，它能够在程序交付测试之前检测出影响系统及其运行环境的一般缺陷、恶意代码及后门程序，能发现编译器不能捕获的错误，很大程度上降低了程序的出错率。但随着软件系统日趋复杂，一般缺陷分析方法已不能满足用户日益增长的需求，其中有两方面的需求尤为突出。首先，一般缺陷分析方法都将缺陷规则内置在缺陷分析工具之中，用户只能选择工具已有的缺陷，不能自行定义缺陷规则；其次，传统缺陷分析方法一般只指出了缺陷发生的最终位置[1]，无法确定实际缺陷与模式缺陷之间的详细对应情况，开发人员仍需手动调试以确定导致缺陷的路径，不能很好地帮助其对错误进行快速排查和修正。

本文结合形式化规约及模型检测中的反例输出技术提出了一种缺陷规则库构建与源码检测方法。利用形式化规约中的模型规约对程序进行建模，用性质规约抽象化待检测缺陷，即从一般控制流结构中提取出适用于缺陷分析的通用原子命题，结合分支时序逻辑CTL的量词集合，构建缺陷规则库元数据。用户可按照分支时序逻辑CTL的语法规则选取原子命题构建积木式静态缺陷集。规则库引擎从缺陷集中拆分出元数据以设计表示静态缺陷的CTL判定公式，形成相关原子命题，从源程序中抽取控制流信息并激活相关原子命题的标记模块，并将控制流信息转换为模型检测可接受的K ripke结构。最后，结合NuSMV模型验证器对转换所得的有限状态系统进行检测，若存在某种缺陷，则返回带有源程序行信息的反例路径。

2 缺陷规则库整体框架

作为一种形式化的自动验证方法，模型检测将“一个有限状态系统是否满足某种规范”抽象为“一个结构是否满足某个命题逻辑公式”，若不满足则返回导致该错误的反例[2]。其一般过程分为三步：对系统进行建模；对规约进行时态逻辑描述；利用模型检测工具结合以上两步实现验证。模型检测需要对有限状态系统进行状态检索，经过对各类程序分析方法的研究[3]，本文采用程序控制流分析手段，展开基于形式化规约的缺陷规则库构建。

图1给出了规则库模型的整体框架，从功能角度可将其流程概括为三个步骤，每个步骤涉及到框架中模块间的通信和交互：

步骤1 用户通过元数据自定义所需分析的缺陷规则，加入规则库。

步骤2 导入待检测程序，由规则库引擎抽取其控制流结构，同时从规则集中取得待分析缺陷，经过命题动态匹配和模型转换两个模块实现程序建模以及规则集中缺陷的实例化，得到模型验证器可接受的有限状态系统。

步骤3 通过NuSMV模型验证器对有限状态系统进行检验，通过检测结果转换与输出模块返回检测结果及导致缺陷的反例路径。

图1 整体框架图

步骤1与步骤2是本文的重点。其中，用户通过自定义缺陷规则形成缺陷规则集，该功能的实现采用了积木式设计模式，并设计了相应的匹配机制和逻辑描述形式，使缺陷的抽象化更为灵活。规则库引擎负责元数据匹配机制的动态唤醒和程序与实际缺陷的关系建模，同时完成了模型结构的转换。

3 积木式缺陷规则库模型

缺陷规则库模型的构建基础是对单一缺陷规则的抽象化描述。本文采用时态逻辑描述系统所要满足的规范，在此基础上对缺陷的行为逻辑进行分析，取得构成规则集的通用原子命题集和逻辑量词集，为规则库的积木式构建准备元数据。

3.1 缺陷的行为抽象

时态逻辑是一种包含有时间概念的逻辑，是在命题逻辑的基础上加入了时态算子而形成的逻辑，其基本组成元素为：原子命题、逻辑连接词、时态连接词[4]。CTL即分支时序逻辑，是一种典型的时态逻辑，缺陷规则库的构建需要用户理解缺陷抽象为CTL公式的过程以实现缺陷自定义，通过分析M itre通用缺陷列表[5]（Common Weakness Enumeration，CWE），不难发现程序缺陷产生的原因与人为因素、编程语言以及缺陷本身都具备一定关联，即缺陷的产生与缺陷本身具备一定的规律性，对静态缺陷而言，该特点在缺陷的语法及语义特征上尤为明显。根据该特征与CTL分支时序逻辑的相似性，同时考虑到缺陷间不可提取的非共性因素，本文定义了静态缺陷的一般缺陷模式，使针对缺陷的CTL抽象过程更为清晰，同时为构造规则库的元数据集提供研究基础。

3.1.1 静态缺陷的一般缺陷模式

通过对静态缺陷语法及语义特征的分析，本文将静态缺陷的一般缺陷模式定义如下：

定义1 基于语法及语义的静态缺陷模式是一个三元组，M=(S，T，C)，其中S表示一个或多个状态，T表示由状态和状态存在性构成的事件，C表示事件发生的范围。

定义2 状态存在性包括：不存在、存在、状态组合逻辑（例如状态间的与或关系）下的存在性。

定义3 缺陷有关事件发生的范围可划分为：全局范围，在某事件之前，在某事件之后，在事件A与事件B之间，直到发生某事件。

以Java语言中的空指针异常为例，其缺陷的语义描述为“对一个不存在的对象调用其属性或方法而导致的异常”，从该描述中可以提取出缺陷模式的基本表示S={s1，s2}，s1表示对象值为null，s2表示调用对象的属性或方法；T={t1，t2}，t1表示“存在”s1，t2表示“存在”s2；C表示事件t1出现在事件t2之前。

3.1.2 缺陷模式与CTL

作为一种非线性的时态逻辑，CTL在命题逻辑的基础上加入了时态算子，同时解决了线性时序逻辑中对所有路径做全程量词的限制。CTL的组成元素包括：原子命题、逻辑连接词、时态连接词及路径量词，其巴克斯范式如下：

其中，F指某个未来状态，X表示下一个状态，G指所有未来状态，U指直到，A指所有路径，E指存在一条路径；ϕ则指某个原子命题，它是CTL的基本单位[6]。举例说明CTL的用法：以started表示开始状态，ready表示就绪状态。则语句“存在一个某未来状态，使得开始状态成立且就绪状态不成立”的CTL描述为：

从CTL的基本描述可以分析得出其与缺陷模式M的对应关系：S映射为原子命题ϕ，T映射为S与逻辑连接词的组合关系，C映射为T与时态连接词和路径量词的组合关系。根据这一对应关系结合CTL的逻辑规则，即可实现缺陷模式的CTL抽象[7]。以静态缺陷分析中的文件输入流关闭异常和空指针异常为例，本文通过以下两步来抽象化缺陷。

步骤1 根据缺陷含义分析缺陷模式，获取相关原子命题。两种缺陷的具体含义为：

（1）文件输入流关闭异常，指在开启了输入流后，没有对其进行关闭而导致的异常。

（2）空指针异常，指对一个不存在的对象（其指针为null）调用其属性或方法而导致的异常。

与以上两种缺陷相关的原子命题，如表1所示。

表1 缺陷及相关原子命题表示

步骤2 根据缺陷模式，确定所要采用的逻辑连接词、时态连接词以及路径量词，得到最终的CTL公式表示形式如下所示。

文件输入流关闭异常：

AG(malloc_fin_s→AF free_fin_s)

该公式的含义：对于任意路径下的所有状态，若某一状态开启了文件输入流s，则任意路径的所有未来状态会存在针对s的文件流关闭操作。

空指针异常：

AG(assign_null_s→!(EFinvoked_s))

该公式的含义：对于任意路径下的所有状态，若某一状态将对象s赋值为null，则不存在未来状态中会调用s的属性或方法的路径。

以上两个步骤可以成功地抽象出缺陷的规则化描述，并能分析出与该规则有关的原子命题和逻辑量词。通过分析缺陷的一般模式，发现大部分原子命题都存在一定的复用性，若在分析过程中进行统一管理与匹配，将显著提高静态缺陷分析的可扩展性，这一发现正是积木式规则库构建的出发点，也是规则库中元数据集的原型。

3.2 积木式构建模式

规则库中会内置缺陷规则的元数据，因为程序分析系统会涉及到大量的实时事件分析，若采用传统的状态机模式处理，会将元数据的事件关联全部写入基本处理逻辑之中，使得程序臃肿不堪，同时严重影响到规则库引擎的响应与处理速度。因此，本文采取积木式构建模式改进这种不足。

积木式构建模式将事件分层，通过简单事件来搭建复杂事件。其特点是通过有限种基本事件模型和有限种组合形式，构造复杂的事件。这使得在处理事件的过程中不用考虑事件间复杂的因果关系，符合人们处理事务时由简单到复杂的行为习惯，使事件的处理更为清晰，更专注于事件的关联与匹配。本文利用积木式构建模式的优点，将与规则有关的所有原子命题和逻辑量词作为底层元数据，通过积木式方法由用户自定义缺陷规则并加入到缺陷规则集中，供规则库引擎调用。

以3.1节中的两种静态缺陷为例，其构成的简易积木式规则库模型如图2所示，其中原子命题集、逻辑量词集、缺陷规则集均以XM L形式描述。原子命题集存储了表1中与缺陷有关的所有原子命题，逻辑量词集存储了缺陷有关的所有逻辑量词，缺陷规则集中存储了CTL形式的由以上两种元素组成的缺陷规则。与此同时，在规则库引擎中会设计原子命题的匹配模块，实现原子命题的动态匹配。

图2 积木式缺陷规则库模型示例图

需要注意的是，与规则集有关的原子命题是原子命题集的一部分，前者由用户输入，后者由系统内置。

规则库引擎中的原子命题动态匹配模块也是积木式模式中的重要组成部分，将在后文中详述。

4 规则库引擎

规则库引擎是缺陷规则库的核心部分，其功能是将导入的待分析程序建模为K ripke结构的有限状态系统，在有限状态系统上动态匹配并标记与规则集关联的原子命题集，再将其转换为模型验证器可接受的数据结构。

4.1 控制流结构抽取与分析

该步骤关联框架中的控制流结构抽取模块和命题动态匹配模块。规则库引擎中源程序的目标模型是一种有限状态系统，有限状态系统的机制是通过状态变量、输入变量和常量来描述不同状态下的不同变量；通过转换关系来描述一个输入如何导致系统从一个状态转换至多个状态；通过条件来描述对系统各可用路径的限制，它符合K ripke结构。

4.1.1 控制流结构与K ripke结构

设计控制流结构抽取模块的原因在于源程序控制流结构与K ripke结构的相似性。程序的控制流图可以用来表示程序的控制流信息，它是一个程序所有可能执行路径的抽象表示，基本元素是节点和有向边，其中节点代表的是无跳转的代码块，有向边是各代码块之间的跳转关系，其数据结构为：

其中，V表示节点有限集，vs表示起始节点，vf表示终结节点，A代表节点间的有向边集合。而K ripke结构是添加了原子命题（AP）概念的有限自动机的变种[8]，其结构如下：

其中，S是有限状态集；I是初始状态集，I⊆S；R是表示状态间转换的二元关系，R⊆S×S；L是标记方法，L:S→2AP，图3是一个简单的K ripke结构范例。

该K ripke结构可描述为：

由此可见，将源程序转换为K ripke结构只需经过两个步骤，首先是从源程序抽取出控制流结构，然后通过遍历控制流节点，对原子命题集中的原子命题进行动态匹配，若某个节点满足某一命题，则在该节点标记该命题为真。

4.1.2 利用Soot抽取及分析控制流结构

直接通过字节码取得控制流会遇到表达式指令不够清晰，表达式树构造过于复杂[9]等情况，本文以Java程序分析为例，选择Soot代替手工分析字节码来抽取和分析控制流。Soot是开源的Java字节码分析与转换工具[10]，既可以作为单独的类优化与检查工具来使用，也可以作为Java字节码的优化与转换框架，其最新版本可支持嵌入集成开发环境，使得程序的分析更为易用和高效。本文在获得控制流结构的同时还需对控制流节点进行分析，因此需要触及到Soot的表现形式并深入到类结构。

首先，要抽取出控制流结构，需要认识Soot的中间表示——IR。Soot提供了四种用于代码分析的中间表现形式，它们分别是：Baf、Grimp、Jimple、Shim ple[11]。每种IR都针对不同的分析做了不同程度的抽象，其中，Jimple是Soot的最主要IR，也是本文抽取和分析控制流信息时的主要操作对象。

由于待分析程序结构的多样化，控制流的抽取也需针对不同场景[12]，Soot构建了五种场景结构：Scene、SootClass、SootM ethod、SootField及Body，分别表示待检测程序本身、某个待检测类、类中的某个方法、类中的某个成员、函数体。Body与不同的IR相对应，本文分析采用了Jimple作为IR，故使用Jim pleBody作为方法的主要载体，以方法为单位，抽取程序的控制流信息。

目前人们多通过Soot的命令行工具和Eclipse插件来查看程序的控制流结构[13]，这不利于在抽取过程中对控制流节点进行分析，因此本文采用了继承Soot的Transformer类并重写其InternalTransform方法来解决该问题，流程如下：

（1）根据取得的JmpleBody，通过getMethod方式取得method。

（2）以Body为参数，通过BriefUnitGraph构建Unit-Graph，得到控制流图的基本结构。

（3）遍历UnitGraph，对每个节点使用getSuccsof遍历分支节点。

由此即可实现控制流结构的抽取及遍历，为下一步原子命题的动态匹配提供基础。

4.2 动态匹配原子命题

原子命题的动态匹配是控制流结构转换的辅助模块，它是在遍历程序控制流节点的过程中，对与规则集相关的原子命题按照一定的匹配规则进行动态匹配。下面将从匹配规则和动态匹配机制两方面介绍该模块。

4.2.1 原子命题匹配规则

图3 K ripke结构

本文详细分析了Jimple之后，发现可以通过Jim ple的声明（Statement）实现原子命题的匹配，因为Jimple是类型化的基于声明的IR，与Java字节码中约200个指令数相比，Jimple只需掌握15种Statement就能更加方便、标准地描述程序。在遍历控制流节点过程中，针对每个节点，取得其Statement类型，以此为基础取得命题匹配条件以及标记命题所需的其他参数，完成原子命题的匹配。

对不同的原子命题而言，其匹配条件也各有不同，前文已经提到，完善功能的系统中会内置与一般缺陷或某一类缺陷有关的所有原子命题，构成原子命题集。因此，需要为原子命题集中的每种命题定义匹配规则。以图2中的原子命题集为例，其对应的匹配条件如表2。

表2 原子命题的Jim ple匹配条件

文中，原子命题的匹配与缺陷类型是分开的，在原子命题集体积较小时，原子命题的匹配机制并不会对规则库引擎的处理速度造成很大影响，但随着原子命题集涵盖范围逐渐变广，则需要定义更为高效的动态匹配机制。

4.2.2 改进的原子命题匹配机制

常见的元素匹配机制是通过分支判定语句if-else进行逐层比对，直至进入判定结果为真的分支，该做法存在三方面的隐患：

（1）当待判定元素过多时，将会相应产生更多的判定语句，这可能会导致某些元素要经过很长的时间才能进入其判定分支，影响处理速度。

（2）若判定分支中的处理语句过于复杂，当判定元素过多时，会造成判定程序体积过大。

（3）判定程序与各原子命题的匹配方法耦合性过高，无法有效地管理每种元素的判定规则。

为解决该匹配机制造成的隐患，本文结合IOC思想设计了一种新的匹配方式，基于接口依赖注入的原子命题动态匹配机制。

IOC即控制反转，其中心思想是通过面向对象法则来解耦程序，也称依赖注入[14]，它通过外部实体调控系统内所有对象，在对象创建时返回该对象所依赖的引用。本文实现该机制的方法与规则库的积木式模式相辅相成，为规则库原子命题集中的每个原子命题定义匹配对象APmodelImp，且所有对象都实现通用接口Base-APmodel及其方法checkAP（），作为对应的原子命题匹配方法。在主程序中只需遍历原子命题集，根据命题集中的匹配对象名反射出对象的引用，赋值给通用接口，由通用接口调用匹配方法，具体实现见程序1。

程序1原子命题动态标记算法伪代码

输入：程序控制流信息，原子命题集

输出：标记原子命题的控制流

Begin

for控制流节点node do

for原子命题集元素ap do

根据ap的名称反射出ap对应的匹配类APModelImp；

将APModelImp实例化所得引用赋给BaseAPModel；

i

f BaseAPModel.checkAP（）为真then

创建原子命题标记对象APObject；

关联node与APObject；

将APObject加入标记对象集合APLlist；

end if

end for

end for

end

4.3 模型转换

规则库引擎中模型转换模块的最终目标，是将前两个功能模块所得的K ripke结构转换为NuSMV模型验证器所接受的SMV语言[15]的同时保留程序的控制流节点信息及行信息，构造缺陷集中各缺陷的实例，实现对缺陷和缺陷检测结果的管理。

由此可见，该模块首先要定义符合规则库模型的SMV语言结构，同时需要设计大量数据结构与相应的转换算法。

规则库引擎将本文分析缺陷所需的SMV结构定义为以下四部分，以缺陷实例的构造为入口，设计了对应的数据结构，见表3。这四部分的构造方式如下：

（1）遍历输出NodeLink中的所有控制流节点S；

表3 数据结构

（2）取NodeLink头节点作为初始节点I，遍历并输出NodeLink中每个节点的后继节点，得到状态转换关系R；

（3）遍历APList得到原子命题集合L；

（4）遍历BugList，取出每个BugObject中的AssertionString，获得CTL形式的断言集合A。

以上数据结构均通过在动态匹配模块中遍历控制流节点，分析元数据中的原子命题集与规则集实现其构造。

5 原型系统与实验结果

依据图2中的积木式规则库模型，实现了原型系统以验证本文提出的构造方法的可行性与有效性。首先是规则集的构建，如图4，用户根据元数据来自定义缺陷，同时指定缺陷名称，加入规则集，图中三个列表分别代表从XM L文件转换而来的原子命题集、逻辑量词集和缺陷规则集。列表顶部为编辑区域，用于规则的添加和更新。缺陷规则列表中显示了规则名称和规则的逻辑公式，可以通过点击“edit”或“del”按钮实现规则的编辑和删除；点击“添加规则”按钮，实现规则的添加。

图4 原型系统-规则库管理

添加规则成功后，即可进入原型系统的检测界面，如图5，左侧是被检测的源程序，首先根据缺陷集和元数据集对源程序进行建模，得到SMV结构的有限状态系统，建模结果如程序2（由于建模结果较长，只截取其中代表性的部分）。建模结果的VAR标签下输出源程序的全部控制流节点，ASSIGN标签下输出控制流节点的转换关系，DEFINE标签下输出已标记的原子命题同时指出原子命题标记的控制流节点。

程序2建模结果

MODULE main

VAR

state：{stat0，stat1，…，stat15}；

ASSIGN

图5 原型系统-输入流关闭异常的反例路径

init（state）：=stat0；

next（state）：=case

state=stat0：{stat1}；

state=stat1：{stat2}；

state=stat2：{stat3}；

state=stat3：{stat4，stat6}；

state=stat4：{stat5}；

...

state=stat14：{stat15}；

TRUE：state；

esac；

DEFINE

param_r0：=state in{stat0}；

assign_null_n0：=state in{stat1}；

invoked_r0：=state in{stat2}；

invoked_n0：=state in{stat6}；

malloc_fin_r1：=state in{stat7}；

free_fin_r1：=state in{stat10}；

if_null_r0：=FALSE；

图5中右侧为检测结果，源程序共检测出三个缺陷，分别为空指针异常NullException，文件输入流关闭异常InputException以及入参判空异常Param IfNullException。点击缺陷条目，在“Counter Example”区域会显示反例路径，同时代码区域会标记反例行信息。反例路径中的每个节点以按钮方式显示，以节点名加行号作为按钮名称，通过点击节点按钮，可以定位到代码中该节点对应的行，从而实现反例重现。从反例路径可以很容易得出导致输入流未关闭异常的原因：在行12处开启了输入流后，跳转至catch块继续执行至结束，因而导致输入流未关闭。

空指针异常的反例路径如图6所示。可以得出导致缺陷的原因是在行5处将变量赋值为null，当args.length小于或等于0时，程序运行到行9，造成空指针异常。

图6 原型系统-空指针异常的反例路径

入参判空异常的反例路径如图7，其含义是指“因方法入参变量在引用前未进行判空而可能引发的空指针异常”，其CTL公式的表示形式为：

AG(param&EF invoked-＞A[!invoked U if_null])其中原子命题param表示方法的输入参数，invoked指引用对象的属性或方法，if_null表示判断对象是否为空值。该CTL描述的语义是“对任意路径下的所有状态，若某一个状态定义了方法的入参变量且未来存在一个状态对该变量进行了引用，则直到对变量判空之前不会对该变量进行引用”。由图7可以得出，方法入参args在第6行引用其length属性之前没有进行判空，若传入的args为空则会导致空指针异常。

图7 原型系统-入参判空异常的反例路径

为进一步验证方法的适用性，以开源软件JBoss中的部分代码作为检测范例。从图8中可以发现，原型系统检测出一条空指针异常。导致缺陷的原因是：在行20处将对象response置为null后，在行27调用了其方法，由此引发空指针异常。

图8 原型系统-JBoss代码检测结果

实验结果表明，可以利用元数据集合中的原子命题将缺陷成功抽象为CTL表示，实现积木式缺陷规则集的构建；待检测程序经过模型抽取、标记与转换过后能够成功检测出存在的缺陷，实现反例路径跟踪。

同时，在分析实验结果的过程中也发现，与其他基于静态分析技术的源码检测工具类似，本文提出的方法不能处理动态代码关联的原子命题，因此不可避免地会出现检测结果的漏报与误报。此外，检测的准确性还依赖于控制流图的准确构建及状态到原子命题的映射。可通过使用高效且准确的控制流抽取方法以及清晰的控制流节点的中间表示形式从外部来降低这两种依赖性带来的隐患；细化原子命题匹配规则及缺陷的逻辑描述，减少静态分析方法可控范围内的漏报与误报。

6 结束语

从形式化规约的角度出发，构建积木式缺陷规则库，在研究过程中实现了规则集的自动构建；源程序到有限状态系统的动态建模；结合规则集和NuSMV模型检测器进行模型检查，返回带有源程序行信息的缺陷路径，实现原型系统验证了本文方法的有效性。

在当前的基础上，仍需进一步研究的问题是：对不同原子命题的匹配规则进行分析，提取共性部分，为存在共性的原子命题制定通用转换规则，提高匹配效率及匹配准确性；扩充原子命题集，以扩大缺陷检测的覆盖率，进一步提升软件的可用性。

[1]A rtzi S，Kiezun A，Dolby J，et al.Finding bugs in Web applications using dynamic test generation and explicitstate model checking[J].IEEE Transactions on Software Engineering，2010，36（4）：474-494.

[2]Ball T，Levin V，Rajamani S K.A decade of software model checking with SLAM[J].Communications of the ACM，2011，54（7）：68-76.

[3]Yoo J，Jee E，Cha S.Formal modeling and verification of safety-critical software[J].Software，2009，26（3）：42-49.

[4]Choppy C，K lai K，Zidani H.Formal verification of UML state diagrams：a petri net based approach[J].ACM SIGSOFT Software Engineering Notes，2011，36（1）：1-8.

[5]Slåtten V，K raemer F A，Herrmann P.Towards automatic generation of formal specifications to validate and verify reliable distributed systems：a method exemplified by an industrial case study[J].ACM SIGPLAN Notices，2012，47（3）：147-156.

[6]Cordeiro L，Fischer B，Marques-Silva J.SMT-based bounded model checking for embedded ANSI-C software[J].IEEE Transactions on Software Engineering，2012，38（4）：957-974.

[7]Ljungkrantz O，Akesson K，Fabian M，et al.Formal specification and verification of industrial control logic components[J].IEEE Transactions on Automation Science and Engineering，2010，7（3）：538-548.

[8]Fioravanti F，Pettorossi A，Proietti M，et al.Generalization strategies for the verification of infinite state systems[J].TPLP，2013，13（2）：175-199.

[9]Liu P，Zhang C.Pert：the application-aware tailoring of java object persistence[J].IEEE Transactions on Software Engineering，2012，38（4）：909-922.

[10]FitzRoy-Dale N，Kuz I，Heiser G.Architecture optimisation with currawong[J].ACM SIGCOMM Computer Communication Review，2011，41（1）：115-119.

[11]Zhou C，Frankl P.JDAMA：Java database application mutation analyser[J].Software Testing，Verification and Reliability，2011，21（3）：241-263.

[12]Eichberg M，Sewe A.Encoding the Java virtual machine’s instruction set[J].Electronic Notes in Theoretical Computer Science，2011，264（4）：35-50.

[13]Girard A，Pola G，Tabuada P.Approximately bisimilar symbolic models for incrementally stable switched systems[J].IEEE Transactions on Automatic Control，2010，55（1）：116-126.

[14]Chang C，Lu C.Pattern-based framework for modularized software development and evolution robustness[J].Information and Software Technology，2011，53（4）：307-316.

[15]A rcaini P，Gargantini A，Riccobene E.A model advisor for NuSMV specifications[J].Innovations in Systems and Software Engineering，2011，7（2）：97-107.