基于面向特征编程范式的形式化验证技术的应用

摘　要：本文系统详尽阐述了FOP编程范式的思想，通过类比，指出FOP与面向方面编程范式的异同。同时还说明FOP给形式化验证技术带来的挑战。本文还比较了现有的FOP形式化验证方法以及我们所做的相关工作的优缺点，并对FOP形式化验证今后可能的研究和发展方向进行讨论。

关键词：编程范式； FOP；面向特征；形式化验证方法
1 引言
　　在面向对象软件开发过程中，开发者常常面临所开发的类与用户提出的需求无法直接对应的问题。这种无法直接对应的问题的根源在于OO（Object Oriented）编程范式是基于系统的参与者来对系统进行划分的，其中类封装的是系统的actor。可在功能的实现过程中，往往需要由多个参与者的参与，这就导致了此类的现象的出现。
　　由于O0编程范式的这种所谓的“局限性”，面向特征编程范式(FOP)应运而生。FOP将特征进行了重新定义，且提出一种新的软件模块分别对特征进行封装，这是的特征就可以理解为用户可以直接感受到的软件功能项。其中，actor与特征的关系是一种相互正交的关系，即每个actor往往参与多个特征的实现，同时每个特征的实现都要涉及多个actor的参与。
2 FOP验证面临的考验
　　FOP面临的考验主要是：1）FOP为匹配传统模块，需要对传统的组合验证首先就要进行属性分解，由于属性分解过程大都依赖验证人员的经验，很难自动化完成，当人工分解不恰当时，就有可能形成循环依赖，最终导致验证的失败。2）基于FOP组合验证比传统组合验证比较难，考验概括为三个步骤：首先，局部化地验证某FOP程序或特征模块是否满足待验证属性；同时，验证同时为该FOP程序或特征模块形成一组约束条件；最后，组合时验证被组合的其他特征模块是否满足这组约束条件。
3 基于 Fisler 经典方法
3.1基于Fisler算法的FOP程序模型
　　在本文第二节我们就对FOP程序进行了递归定义。我们对FOP有了简单了解。在基于Fisler算法的FOP程序模型中，以状态机片段表示mixin ,Fisler以状态机表示actor。形式化定义如下：
　　定义mixin：mixin是一个多元组，其中∑是输入字母表；△是输出字母表；S是mixin的状态集合等。
　　定义actor：一个actor M是一个多元组，其中△是输出字母表，S是actor的状态集合，R s×PL(∑)×S是迁移关系，S0∈S是初始状态。其中L：s是标记函数，表示每个状态上为真的那些输出符号，PL(∑)表示以上的命题逻辑公式集合。
3.2 Fisle的验证方法
　　从定义出发，针对上述模型，Fisler给出了相应的模型检验方法，且检验方法符合增量式验证框架体系。在此，我们只讨论特征模块和FOP程序都只包含一个元素的情况。基于定义actor的并行组合和定义局部组合，多元素的情况完全可以转换为单状态机进行验证。
　　算法1 形成约束 我们首先要设接口为，同时要设基程序B，二者设计并定义好后，等待验证属性。
　　(1)首先验证B是否满足规则，通过使用标准的CTI 模型检验算法实现。
　　(2)在整个验证过程中，将标记在reentry和exit上的标记集存储下来。
　　(3)对规则的所有有问题的子公式，拿到B上验证AG，验证AG即验证从exit到reentry的每条路径上是否先于exit成立。如果验证失败，就说明了存在路径，则即记录Until Check值为true。
　　算法2 保持验证 设mixin E= 。
　　(1)将mixin中in上的标记统一设为exit状态上的原子命题。
　　(2)除特殊条件外，用标记在reentry状态上的每一个公式F来标记out状态。
　　(3)依据一定的顺序，对标记在exit状态上的所有非原子命题公式F。
　　(4)最后通过判断exit上的标记与in上的标记是否相同。如果结果相同，则验证成功，B与E的组合不会改变待验证属性；如果结果不同，则需要对全局组合进行验证，验证失败。为更好地阐明上述算法的思想，我们还可以在框架内引入几个Nguyen的定义，帮助我们更好的进行验证。
3.3 Nguyen的保持验证算法
　　Nguyen的保持验证算法主要步骤可以这样描述：首先我们要对E的out状态进行描述，通过引入任意的E的函数作为out上的标记。同时，将in上的标记设为ex状态上的原子命题，并且在E上执行模型的检验程序。检查对于任意B和任意E的状态检查是否成立。若re在B中不是ex的祖先，则属性保持，验证成功。反之，如果状态的检查不成立，则属性是否保持无法确定，算法结束，验证失败。通过以上步骤我们对Nguyen的保持验证算法有了详细的了解。
4 Fisler方法扩展
　　虽然Fisler建立了FOP程序的第一个形式化模型，同时也提出了相应的验证算法，但是，例如特征之间的循环依赖问题、mixin对actor的行为覆盖问题、原子命题的演进性、全局性以及局部性问题等，被形式化模型所忽略。本节给出了这些问题的解决方案（即Fisler方法的扩展）。
4.1 Li验证算法
　　各个特征模块的开发是相对独立的，这是由FOP的开发思想决定。这种独立性导致各个特征模块的AP集合也是局部的，其中的任何一个特征模块并不知道其它特征模块定义了哪些原子命题。但作为Fisler方法在局部验证时，其隐含地要求使用的是全局AP集合，否则保持验证将终止，且无法确定它们的取值。
　　为解决Li指出的命题的全局性与局部性问题，我们将命题划分为Data Proposition和 Control Proposition（即数据命题和控制命题）。数据命题DP是关于数据共享的，它具有持续性的特点。即其在某个状态成立，DP就沿着程序的执行路径一直“走”下去，直到另一个状态（基于此路径）对其做出显式的改变；控制命题CP则与DP相反，其主要对应用户的选择具有瞬时性的特点。除了那些存在用户交互的状态以外，这些操作默认在所有的状态都是不成立的，例如按下某个按钮等。通过引入了3值模型检验，Li最终解决了这个问题。
4.2 Nguyen验证算法
　　Nguyen扩展了Fisler的FOP模型只支持单出口与单入口状态的mixin模型，Nguyen允许mixin存在多个入口状态和多个出口状态。另外， Nguyen的模型也支持行为覆盖和行为添加，这点与Blundell和Li的模型都是一样的。Nguyen针对这个模型，还给出了自己的验证算法 （本文3．2节中给出了该算法针对单入口与单出口状态裁剪后的经典版本）。
4.3 Blundell验证算法
　　数据命题虽然具有可持续的特性，但它可能起源于其他特征模块，也可能起源于基程序，这就导致了局部验证很难确定。在局部验证过程中，Blundell只是生成一个参数 化的约束条件，Blundell自身并不生成确定的结果，该约束条件直到组合时和保持验证时才被解除，因此我们便可以得到具体的验证结果。这样的实现可以避免使用3值逻辑模型检验引入的不确定性因素。
4.4 Wang验证算法
　　无论是Li验证算法还是Blundell验证算法，他们所给出的特征模块组合过程都不支持特征问的循环依赖，为了支持循环依赖，Wang验证算法对Blundell方法进行了延续性的扩展。具体思路如下：
　　首先，将每个特征视为一个抽象状态，并以Blundell方法生成的约束条件作为该抽象状态上的标记；
　　其次，抽象状态之间的迁移关系也即是特征问题的依赖关系，同时形成一个状态机（主要由这些抽象状态构成的）；
　　最后，在形成状态机上进行模型检验。
　　从对比中我们可以发现，Wang验证算法是Blundell验证算法的延续和扩展，对于验证算法本身有着非常重大的意义。
5 基于层次状态机的验证算法
　　Ye提出以层次状态机(Hierarchical State Machine)是作为AFM的程序模型，与前面都使用状态机作为FOP程序的模型是完全不同的。AFM 由于借鉴了FOP思想体系，因此我们完全可以使用FOP程序验证Ye方法。其中Ye方法的局部验证使用了HSM经典模型检验算法，在验证过程中，它收集了各子状态机所属集合作为其约束条件，其中状态机所属集合包括YES集合、NO集合或者MAYBE集合等。HSM经典模型检验算法保持验证的基本思想。
6 结束语
　　通过以上的介绍，可以确定今后的研究方向，主要包括以下两点：(1)作为FOP模型的相关验证技术，我们可以采用HSM方式。(2)可以借鉴程序切片的相关技术，因为特征模块对功能的封装与程序切片技术有很多相似之处。 本文链接：http://www.qk112.com/lwfw/jsjlw/jisuanjiyingyong/242499.html