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

《基于面向特征编程范式的形式化验证技术的应用与研究》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、基于面向特征编程范式的形式化验证技术的应用与研究本文系统详尽阐述了FOP编程范式的思想，通过类比，指出FOP与面向方面编程范式的异同。同时还说明FOP给形式化验证技术带来的挑战。本文还比较了现有的FOP形式化验证方法以及我们所做的相关工作的优缺点，并对FOP形式化验证今后可能的研究和发展方向进行讨论。关键词：编程范式；FOP；面向特征；形式化验证方法1引言　　在面向对象软件开发过程中，开发者常常面临所开发的类与用户提出的需求无法直接对应的问题。这种无法直接对应的问题的根源在于OO（ObjectO

2、riented）编程范式是基于系统的参与者来对系统进行划分的，其中类封装的是系统的actor。可在功能的实现过程中，往往需要由多个参与者的参与，这就导致了此类的现象的出现。　　由于O0编程范式的这种所谓的“局限性”，面向特征编程范式(FOP)应运而生。FOP将特征进行了重新定义，且提出一种新的软件模块分别对特征进行封装，这是的特征就可以理解为用户可以直接感受到的软件功能项。其中，actor与特征的关系是一种相互正交的关系，即每个actor往往参与多个特征的实现，同时每个特征的实现都要涉及多个ac

3、tor的参与。2FOP验证面临的考验　　FOP面临的考验主要是：1）FOP为匹配传统模块，需要对传统的组合验证首先就要进行属性分解，由于属性分解过程大都依赖验证人员的经验，很难自动化完成，当人工分解不恰当时，就有可能形成循环依赖，最终导致验证的失败。2）基于FOP组合验证比传统组合验证比较难，考验概括为三个步骤：首先，局部化地验证某FOP程序或特征模块是否满足待验证属性；同时，验证同时为该FOP程序或特征模块形成一组约束条件；最后，组合时验证被组合的其他特征模块是否满足这组约束条件。3基于Fis

4、ler经典方法3.1基于Fisler算法的FOP程序模型　　在本文第二节我们就对FOP程序进行了递归定义。我们对FOP有了简单了解。在基于Fisler算法的FOP程序模型中，以状态机片段表示mixin,Fisler以状态机表示actor。形式化定义如下：　　定义mixin：mixin是一个多元组，其中∑是输入字母表；△是输出字母表；S是mixin的状态集合等。　　定义actor：一个actorM是一个多元组，其中△是输出字母表，S是actor的状态集合，Rs×PL(∑)×S是迁移关系，S0∈S是

5、初始状态。其中L：s是标记函数，表示每个状态上为真的那些输出符号，PL(∑)表示以上的命题逻辑公式集合。3.2Fisle的验证方法　　从定义出发，针对上述模型，Fisler给出了相应的模型检验方法，且检验方法符合增量式验证框架体系。在此，我们只讨论特征模块和FOP程序都只包含一个元素的情况。基于定义actor的并行组合和定义局部组合，多元素的情况完全可以转换为单状态机进行验证。　　算法1形成约束我们首先要设接口为，同时要设基程序B，二者设计并定义好后，等待验证属性。　　(1)首先验证B是否满足规

6、则，通过使用标准的CTI模型检验算法实现。　　(2)在整个验证过程中，将标记在reentry和exit上的标记集存储下来。　　(3)对规则的所有有问题的子公式，拿到B上验证AG，验证AG即验证从exit到reentry的每条路径上是否先于exit成立。如果验证失败，就说明了存在路径，则即记录UntilCheck值为true。　　算法2保持验证设mixinE=。　　(1)将mixin中in上的标记统一设为exit状态上的原子命题。　　(2)除特殊条件外，用标记在reentry状态上的每一个公式F来

7、标记out状态。　　(3)依据一定的顺序，对标记在exit状态上的所有非原子命题公式F。　　(4)最后通过判断exit上的标记与in上的标记是否相同。如果结果相同，则验证成功，B与E的组合不会改变待验证属性；如果结果不同，则需要对全局组合进行验证，验证失败。为更好地阐明上述算法的思想，我们还可以在框架内引入几个Nguyen的定义，帮助我们更好的进行验证。3.3Nguyen的保持验证算法　　Nguyen的保持验证算法主要步骤可以这样描述：首先我们要对E的out状态进行描述，通过引入任意的E的函数作

8、为out上的标记。同时，将in上的标记设为ex状态上的原子命题，并且在E上执行模型的检验程序。检查对于任意B和任意E的状态检查是否成立。若re在B中不是ex的祖先，则属性保持，验证成功。反之，如果状态的检查不成立，则属性是否保持无法确定，算法结束，验证失败。通过以上步骤我们对Nguyen的保持验证算法有了详细的了解。4Fisler方法扩展　　虽然Fisler建立了FOP程序的第一个形式化模型，同时也提出了相应的验证算法，但是，例如特征之间的循环依赖问题、mixin对actor的行为覆盖问题、原子