一种基于模型的侵入式灰盒组装验证方法

摘要

本发明涉及一种基于模型的侵入式灰盒组装验证方法，属于软件工程技术领域，包括步骤：1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模型；2)实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中检索，并确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位置，若为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置；3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行的Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。与现有技术相比，本发明具有提高基于构件的软件开发效率等优点。

说明书

技术领域

本发明涉及一种软件工程技术，尤其是涉及一种基于模型的侵入式灰盒组装 验证方法。

背景技术

基于构件的软件开发(Component-Based Software Development,CBSD)是软件 工业化的大趋势。计算机软件构架由手工代码开发模式转变为重用可独立运行的、 被封装的构件模式，它具有更高的灵活性。由于复用算法和软件功能，基于构件的 软件开发大大缩短了软件系统的开发进度，尤其是在经费有限的情况下该方法是实 现软件项目开发的最佳选择。

构件是将具有特定功能的模块或代码按照一定的格式进行封装。构件组装则是 研究如何组装构件的机制，以需求模型为基础，查找合适的构件进行集成以快速开 发系统软件为目的。目前，构件组装技术主要分为黑盒组装方法，白盒组装方法和 灰盒组装三种方法。但各自存在优缺点：黑盒组装方法不需要对构件的实现细节有 任何了解，也不需要对构件进行配置或修改，但“以不变的构件组装成万变的应用” 的理念过于现实化，实际应用难度大。黑盒组装对功能进行抽象描述，使用户无法 了解构件是如何运行的，缺乏对黑盒构件的可信性。白盒组装方法则要求将构件的 所有实现细节都展示出来，让复用者理解后再进行组装，并可按应用需求对构件进 行二次修改，但该方法需要用户对实现细节和具体需求了如指掌，在程序可读性和 可维护性方面存在应用的局限性。而灰盒组装方法介于黑盒和白盒之间，其通过混 合使用组装机制来架构系统软件实现用户组装需求，既灵活又高效。因此，灰盒组 装方法是目前构件组装技术的研究重点和难点。

在灰盒组装过程中，即要体现构件的部分实现细节，又要展示构件的部分模块 功能。实际上，构件组装的操作更加复杂，而且组装的正确性和安全性很难保证。 涉及如下两个主要问题：

1)如何描述和表达灰盒组装的组装流程？包括展示部分实现细节和部分功能 模块。

2)如何有效地对灰盒组装进行验证？包括构件组装的正确性和安全性。

在传统的组装场景上，每个组装点的功能需求以push推的形式向构件库发出 构件检索请求，查询是否存在合适的构件，同时以pull拉的形式将目标实例构件 插入到组装点进行集成。这种方式目标明确，组合速度块。但在实际情况下，存在 如下问题：

1)由于缺少构件规格说明语言，很难正确地、形式化地描述push点的构件需 求；

2)由于构件库中的构件数量有限，很难准确地检索出满足请求的单个构件实 体。

因此需要一套系统的基于侵入式组装方式，允许构件以主动的方式进行组合以 满足目标组装点的功能需求。无论是原子构件还是复合构件，其通过一种侵入 (intrusion)的方式强行插入到组装点。虽然，侵入式组装可以弥补传统构件组装的 不足，但同样存在一些问题：

1)从实现细节的源代码级来看，侵入式组装将增加一些无用代码或危险代码；

2)从组装高层的工作流来看，侵入式组装将附加一些无用的接口或威胁接口。

针对这些组装问题，一方面需要保证构件交互的正确性，即对局部而言，交互 接口中的参数，参数顺序等是兼容的；另一方面需要保证组合的构件是安全性的， 即对整体而言，不存在隐藏的威胁，不存在违反既定的需求。而模型检验作为测试 的辅助手段，是一种自动化的、基于有限状态模型的性质验证方法，它通过显式的 状态搜索或隐式的不动点计算来检测系统模型是否满足预期性质，当模型不满足性 质时输出反例信息，即模型中违背性质的状态迹。基于此，将模型检验方法应用检 验基于侵入式的灰盒组装方法组装的软件，可以有效地验证构件组装过程的正确性 和安全性，保证基于构件的软件系统的软件质量。

发明内容

本发明的目的就是为了克服上述现有技术存在的缺陷而提供一种基于模型的 侵入式灰盒组装验证方法。

本发明的目的可以通过以下技术方案来实现：

一种基于模型的侵入式灰盒组装验证方法，包括步骤：

1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作 流模型；

2)实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中 检索，并确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象 构件所在位置，若为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所 在位置；

3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV 执行的Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。

所述实例构件库的构建过程包括步骤：

A1：将Java程序进行封装使其构件化，添加组装点，并采用反射技术解析出 程序功能的函数方法，以及组装点的接口信息；

A2：根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参 数名称，参数类型和参数顺序。

A3：将解析出的函数方法进行绑定，产生调用关系；

A4：将构件化后的Java程序以XML形式保存，输出实例构件的封装文件；

A5：将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封 装文件中标识其相关的应用领域，以提供构件组装时使用。

所述步骤1)具体包括步骤：

11)新建组装界面，根据待开发软件的业务逻辑绘制工作流；

12)设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。

13)在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止 点。

所述步骤2)中将单一实例构件插入至抽象构件所在位置的过程具体为：根据 工作流调用关系，绑定该实例构件与相邻抽象构件实例化得到的实例构件间的接口 参数，包括参数名称，参数类型，以及参数顺序。

所述步骤2)中选择多个实例构件组合为复合构件并侵入至抽象构件所在位置 的过程中：

以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件集 合，使得多个实例构件在组合后，既满足接口信息，又满足领域应用的要求；或

以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得 多个实例构件在组合后，既满足接口信息，又满足领域应用的要求。

所述步骤3)具体包括：

31)根据实例化配置信息，输出相应的配置文件；

32)转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本；

33)检验组装构件是否满足正确性和安全性；

34)通过执行模型检验器NuSMV对结构脚本执行检验，根据检验结果判断组 装是否满足正确性和安全性。

所述步骤31)具体包括步骤：

311)新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的 名称和功能；

312)根据配置信息的接口定义部分，解析接口信息，并将解析得到的接口信 息写入该组装构件的接口定义部分；

313)根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用 于描述构件调用关系，将调用关系写入该组装构件的工作流定义部分。

314)使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关 系，同时标记组装点与下层构件之间的侵入关系。

315)对配置文件进行语法检验，确保每个抽象构件都被实例化。

所述步骤32)具体包括步骤：

321)根据组装构件内部的实例构件的名称信息，得到转化的状态集；

322)根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子 命题；

323)根据工作流上的调用关系，转化为状态迁移关系；

324)根据状态集、原子命题和状态迁移关系，构造Kripke结构的可验证脚本。

325)对可验证脚本进行语法检验，确保组装语法是正确的。

所述步骤33)具体包括步骤：

331)从接口信息中接口参数覆盖准则出发，检验侵入式组装的正确性；

332)检验组装构件是否有空接口没被使用；

333)从功能迁移覆盖的角度出发，检验侵入式组装的安全性；

334)检验组装构件是否有功能存在不可终止性。

所述步骤34)具体为：

通过执行模型检验器NuSMV对结构脚本执行检验，并根据检验结果判断构件 组装过程是否满足正确性和安全性，若为是，则将其配置文件输出并保存到构件库 中，同时标记组装构件的功能和应用领域属性，若为否，则执行提示错误信息。

与现有技术相比，本发明具有以下优点：

1)本发明在无法找到合适的单一实例构件时，采用将多个实例构件组合侵入 至指定位置，可以提高软件的开发效率，解决了抽象构件实例化时无法找到合适的 单一构件的问题。

2)，应用模型检验技术检验构件组装的配置文件，此种采用模型检验方法可以 实现自动化检验灰盒组装正确性和安全性的目的。

3)侵入过程以领域和功能作为基点，可以增加侵入过程的匹配度。

附图说明

图1为本发明的侵入式灰盒组装验证流程图；

图2为本发明的构件侵入方式表示图；

图3为一个下层构件侵入上层构件的模型示例；

图4为本发明的构件组装架构图；

图5为本发明的构件配置文件结构图；

图6为本发明的组装检验执行流程。

具体实施方式

下面结合附图和具体实施例对本发明进行详细说明。本实施例以本发明技术方 案为前提进行实施，给出了详细的实施方式和具体的操作过程，但本发明的保护范 围不限于下述的实施例。

一种基于模型的侵入式灰盒组装验证方法，如图1所示，首先，采用反射技术 针对Java可执行程序进行解析，添加内部流程逻辑与组装点，并添加组装点，封 装入构件库。其次，用户根据需求在可视化界面设计抽象工作流。接着，针对工作 流，在服务库中检索可满足的单一实例构件。如果不存在满足的实例构件，则采用 算法将多个实例构件按照一定的组合方法侵入到组装点。抽象构件实例化的结果是 得到组装配置文件。然后，转化配置文件得到适合于模型检验器NuSMV执行的 Kripke结构脚本。根据不同覆盖准则产生检验性质，检验构件组装的正确性和安全 性。最后，反馈用户检验结果。

其中，实例构件库的构建过程包括步骤：

A1：将Java程序进行封装使其实例构件化，添加组装点，并以.class为后缀名 的可执行代码采用反射技术解析出程序功能的函数方法，以及组装点的接口信息；

A2：根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参 数名称，参数类型和参数顺序；

A3：在可视化图形编辑器上，将解析出的函数方法进行绑定，产生调用关系， 具体包括步骤：

A31：在可视化编辑器上显示当前实例构件，用实线圆形图形元素表示函数方 法。

A32：拖动连接线绑定具有前后顺序关系的接口。

A33：添加其他图形元素描述该构件内部流程，用虚线圆形表示功能实体是内 部不可见的功能。

A34：若当前构件是可继续组装扩展的，则用菱形表示可待插入其他构件的组 装点。

A4：将构件化后的Java程序以XML形式保存，并产生一个以.des为后缀的 描述文件作为实例构件封装文件；

A5：将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封 装文件中标识其相关的应用领域，以提供构件组装时使用。

具体的，组装验证方法包括步骤：

1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作 流模型，具体包括步骤：

11)新建组装界面，根据待开发软件的业务逻辑绘制工作流，具体为：在新建 的组装界面上，切换到工作流图形化编辑模式后，根据组装需求，拖动图形元素绘 制组装的工作流；

12)设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。

13)在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止 点。

14)以.wf为文件后缀名，保存工作流模型。

2)实例化：根据工作流中各抽象构件的功能要求和接口信息在库中检索，并 确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在 位置，若为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置， 具体包括步骤：

21)切换到组装场景实例化功能界面，筛选实例构件，具体步骤如下：

211)点击工作流上的抽象构件，从该构件抽象描述信息中读取构件需求描述；

212)根据构件领域需求选取实例构件集合；

213)根据构件功能描述筛选实例构件集合；

214)根据数据参数个数，筛选满足参数个数的实例构件集合；

215)根据数据参数类型，筛选满足参数类型的实例构件集合；

216)根据数据参数顺序，筛选满足参数顺序的实例构件集合；

217)执行步骤211)至步骤216)后，对实例构件集合中的构件进行排序。

22)确认是否存在匹配的单一实例构件，若为是，则执行步骤23)，若为否， 则执行步骤24)；

23)根据工作流调用关系，绑定该实例构件与相邻抽象构件实例化得到的构件 间的接口参数，包括参数名称，参数类型，以及参数顺序，具体步骤如下：

231)在抽象构件的属性编辑区域，将该实例构件绑定到相应的抽象构件所在 的图形元素代表的组装点上；

232)根据工作流调用关系，绑定构件间的接口参数，包括参数名称，参数类 型，以及参数顺序；

233)点击保存实例化组装时，检查参数类型和参数顺序是否设置正确。

24)以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件 集合，使得实例构件集合在一定的组合方式下，既满足接口信息，又满足领域应用 的要求；或

以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得 实例构件集合在一定的执行条件下，既满足接口信息，又满足领域应用的要求。

图2给出了四种组合行为的侵入式组装方法。侵入的子构件可能不止一个，侵 入的形式也各有不同，这些子构件之间大致存在四种关系：选择，互斥，顺序，并 发。选择和互斥之间区别在于选择可以是若干个构件一起侵入，而互斥是有且仅有 一个满足条件的构件才能够侵入；顺序表示若干构件按顺序一个一个地侵入；并发 关系表示若干子构件在同一时间点一起侵入。图4中C表示主构件，I₁…I_n表示侵 入的子构件。选择采用符号||描述，例如I₁||I₂||…||I_n；互斥采用符号|描述，例如I₁|I₂|… |I_n；顺序采用+描述，例如I₁+I₂+…+I_n；并发采用<>描述，例如I₁<>I₂<>…<>In)。

图3描述了一个下层构件侵入上层构件的数据模型。从结构上分为两层：第一 层描述上层构件a，其存在一条路径，菱形区域q₃表示人为 设计的侵入构件；第二层描述侵入的下层构件之间的关系，其选取的子构件b和c 进行并发可实现组装点q₃的功能。从整体上看，b和c并发组合并以强制的方式侵 入主构件a的组装点q₃。

图4为本发明的构件组装架构图。椭圆形表示构件的接口，菱形表示侵入点， 圆形表示功能模块，箭头表示构件侵入组装方向。可视化层Visual Application展示 工作流Workflow的流程；实例化层Concretization Level组装实例构件；构件层 Component Level则描述构件功能；统一构件库UCR存储实例构件集。分层化地描 述构件之间的关系，形式化表达构件侵入与被侵入构件交互关联；底层为构件层， 构件之间组合可通过构件侵入方式组成框架。由若干个框架构成最终的可视化图形 文件。接口支持各个构件间进行交互。在构件内部流程中，预留了组装点用于构件 侵入式组合，称为外联口。通过外联口体现分层思想，表示在分层构件中，上层构 件在被下层构件侵入时，下层侵入构件通过外联口中参与上层构件的交互。主构件 为最高层，底层的应用以侵入的方式层层插入构件中，因此越底层包含的内容越细 化。

25)为组装点标识组装状态属性，具体步骤如下：

251)为步骤23)完成的抽象构件实例化的节点，标识状态为插入点。

252)为步骤24)完成的抽象构件实例化的节点，标识状态为侵入点，并将该 节点用菱形表示。

253)如果步骤24)仍无法找到合适的实例构件(集)，那么允许在组装点插 入手工编写的具体实现代码。

26)如果插入组装点的实例构件还包含其它组装点，则返回执行步骤21)，使 得组装场景上的抽象构件以及组装点全部完成实例化操作。

3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV 执行的Kripke结构脚本，并基于得带的结构脚本验证构件组装过程的正确性和安 全性，具体包括步骤：

31)根据实例化配置信息，输出相应的配置文件，具体包括步骤：

311)新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的 名称和功能；

312)根据配置信息的接口定义部分，解析接口信息，并将这些信息写入该组 装构件的接口定义部分；

313)根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用 于描述构件调用关系，将调用关系写入该组装构件的工作流定义部分；

314)使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关系， 同时标记组装点与下层构件之间的侵入关系；

315)对配置文件进行语法检验，确保每个抽象构件都被实例化。

图5给出了一个描述构件的配置文件结构图，支持可视化灰盒组装过程涉及的 构件图形化框架的XML配置文件，用于描述构件输入/输出，以及侵入式组装验证。 如下代码所示，给出了构件的Schema模式。

主要分为两个部分的定义，第一部分是关于构件接口的定义，第二部分是关于 构件工作流的定义。

在接口定义：

<xs:element name＝”Interface”type＝”xs:string”maxOccurs＝”unbounded”>… </xs:element>部分，以上XML文件对应的标签解释如表1所示：

表1：

在构件工作流的定义：

<xs:element name＝”Workflow”type＝”xs:string”>…</xs:element>部分，以上 XML文件对应的标签解释如表2所示：

表2

32)转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本， 具体包括步骤：

321)根据组装构件内部的实例构件的名称信息，得到转化的状态集；

322)根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子 命题；

323)根据工作流上的调用关系，转化为状态迁移关系；

324)根据状态集、原子命题和状态迁移关系，构造Kripke结构的可验证脚本；

325)对可验证脚本进行语法检验，确保组装语法是正确的。

33)检验组装构件是否满足正确性和安全性，具体包括步骤：

331)从接口信息中接口参数覆盖准则出发，采用时态逻辑AG(p)性质检验侵 入式组装的正确性；

332)采用命令deadlock检验组装构件是否有空接口没被使用；

333)从功能迁移覆盖的角度出发，采用时态逻辑AF(p)性质检验侵入式组装 的安全性；

334)采用命令livelock检验组装构件是否有功能存在不可终止性。

34)通过执行模型检验器NuSMV对结构脚本执行检验，具体步骤如下：

341)将Kripke结构的脚本输入到模型检验NuSMV中；

342)输入33)步骤得到的用于检验的目标检验性质(集)是否可满足；

342)执行模型检验器NuSMV，并查看执行结果。

35)根据检验结果判断组装是否满足正确性和安全性具体为：通过执行模型检 验器NuSMV对结构脚本执行检验，并根据检验结果判断构件组装过程是否满足正 确性和安全性，若为是，则将其配置文件输出并保存到构件库中，同时标记组装构 件的功能和应用领域属性，若为否，则执行提示错误信息。

图6是本实施例组装检验执行流程。为了将配置文件转化为模型检验器所能接 受的可行执行文件，需要将配置文件进行解析并进行形式化建模和验证。具体步骤 如下：

S1：形式化定义构件配置文件，映射XML标签使其可被机器所理解。具体步 骤如下：

S11：定义构件为五元组IC＝(CN,FD,CD,I,W)，其中CN表示构件名称，FD 描述构件的功能，CD描述构件所属应用领域，I表示构件接口的集合，W表示构件 内部流程行为的集合。

其中CN与XML标签Compoment_Name进行映射关联，FD与XML标签 Functional_Description进行映射关联，CD与XML标签Compoment_Domain进行映射 关联，I与XML标签Interface进行映射关联，W与XML标签Workflow进行映射关联。

S12：定义接口为三元组I＝(IN,ID,IA)，其中IN表示接口名称，ID描述接口的 功能，IA描述接口属性集合。

其中IN与XML标签Interface_Name进行映射关联，ID与XML标签Interface _Description进行映射关联，IA与XML标签Interface_Attribute进行映射关联。

S13：定义接口属性为三远足IA＝(AN,AT,ANU)，其中AN表示接口属性， AT∈{String,Int,Char,Array,Float,Double,Boolean,Map,Byte}表示接口类型， ANU表示是否可以为空。

其中AN与XML标签Attribute_Name进行映射关联，AT与XML标签 Attribute_Type进行映射关联，ANU与XML标签Attribute_Nullable进行映射关联。

S14：定义构件内部流程为三元组W＝(SN,ST,AT)，其中SN为流程状态名称， ST∈{Star,End,Inherent,Insert_Port,Intrusion_Port}为状态类型，AT是迁移关系集 合。

其中SN与XML标签State_Name进行映射关联，ST与XML标签State_Type进行 映射关联，AT与XML标签Action_To进行映射关联。

S15：定义迁移关系为二元组AT＝(ATP,GC)，其中ATP是卫式条件，GC是状 态名称。

其中ATP与XML标签Action_Type进行映射关联，GC与XML标签 Guard_Condition进行映射关联。

S2：根据形式化定义，应用如下算法对配置文件进行解析，主要包括接口解 析算法和工作流解析算法，前者用户获得构件接口基本信息，后者用于解析工作流 得到符合模型检验器语法规则的Kripke结构脚本。具体步骤如下：

S21：根据如下算法解析构件接口。该算法以构件IC作为输入，输出构件接口 信息。其中，集合Map_{I_Name}表示保存的接口名字，针对接口参数进行解析，包括集 合MultiHashMap_{I_Name}表示保存多个接口参数名字，集合MultiHashMap_{A_Type}表示保 存多个接口参数类型，集合MultiHashMap_{I_Nullable}表示保存多个接口参数是否可为 空。

S22：定义目标转化形式化模型。为了实现模型检验，需要将组装配置文件转 化为状态迁移系统Kripke结构描述其行为M＝(S,I,AP,L,T)，其中

1、S是有限的状态集，每一个状态由组装中的构件与其卫式条件构成。

2、是初始状态集。

3、AP是标记状态的原子命题，由接口状态类型决定。

4、是迁移关系集。

5、L:S→2AP是状态标记函数,L(s)表示状态s下所有为真的原子命题集。

S23：根据如下算法解析构件工作流，使其转化为Kripke结构。对灰盒组装配 置文件进行解析构造相应的Kripke结构脚本。该算法以构件高层IC_m作为输入，输 出状态迁移系统。其中，集合SN(w)和ST(w)解析工作流的名称和类型，并当接口 不为空时迭代地解析接口动作Action_To以构造迁移转化关系。

S3：根据覆盖准则产生检验性质。具体步骤如下：

S31：从接口参数覆盖准则出发，采用时态逻辑AG(p)性质检验侵入式组装的 正确性。

S32：采用命令deadlock检验组装构件是否有空接口没被使用。

S33：从功能迁移覆盖的角度出发，采用时态逻辑AF(p)性质检验侵入式组装 的安全性。

S34：采用命令livelock检验组装构件是否有功能存在不可终止性。

S4：将转化后的组装脚本和检验性质输入到模型检验NuSMV中，执行模型检 验器NuSMV。根据检验结果判断组装是否满足正确性和安全性。