一种基于模型的侵入式灰盒组装验证方法
一种基于模型的侵入式灰盒组装验证方法
【技术领域】
[0001] 本发明涉及一种软件工程技术，尤其是涉及一种基于模型的侵入式灰盒组装验证 方法。
【背景技术】
[0002] 基于构件的软件开发（Component-BasedSoftwareDevelopment,CBSD)是软件工 业化的大趋势。计算机软件构架由手工代码开发模式转变为重用可独立运行的、被封装的 构件模式，它具有更高的灵活性。由于复用算法和软件功能，基于构件的软件开发大大缩短 了软件系统的开发进度，尤其是在经费有限的情况下该方法是实现软件项目开发的最佳选 择。
[0003] 构件是将具有特定功能的模块或代码按照一定的格式进行封装。构件组装则是研 宄如何组装构件的机制，以需求模型为基础，查找合适的构件进行集成以快速开发系统软 件为目的。目前，构件组装技术主要分为黑盒组装方法，白盒组装方法和灰盒组装三种方 法。但各自存在优缺点：黑盒组装方法不需要对构件的实现细节有任何了解，也不需要对构 件进行配置或修改，但"以不变的构件组装成万变的应用"的理念过于现实化，实际应用难 度大。黑盒组装对功能进行抽象描述，使用户无法了解构件是如何运行的，缺乏对黑盒构件 的可信性。白盒组装方法则要求将构件的所有实现细节都展示出来，让复用者理解后再进 行组装，并可按应用需求对构件进行二次修改，但该方法需要用户对实现细节和具体需求 了如指掌，在程序可读性和可维护性方面存在应用的局限性。而灰盒组装方法介于黑盒和 白盒之间，其通过混合使用组装机制来架构系统软件实现用户组装需求，既灵活又高效。因 此，灰盒组装方法是目前构件组装技术的研宄重点和难点。
[0004] 在灰盒组装过程中，即要体现构件的部分实现细节，又要展示构件的部分模块功 能。实际上，构件组装的操作更加复杂，而且组装的正确性和安全性很难保证。涉及如下两 个主要问题：
[0005] 1)如何描述和表达灰盒组装的组装流程？包括展示部分实现细节和部分功能模 块。
[0006] 2)如何有效地对灰盒组装进行验证？包括构件组装的正确性和安全性。
[0007] 在传统的组装场景上，每个组装点的功能需求以push推的形式向构件库发出构 件检索请求，查询是否存在合适的构件，同时以pull拉的形式将目标实例构件插入到组装 点进行集成。这种方式目标明确，组合速度块。但在实际情况下，存在如下问题：
[0008] 1)由于缺少构件规格说明语言，很难正确地、形式化地描述push点的构件需求；
[0009] 2)由于构件库中的构件数量有限，很难准确地检索出满足请求的单个构件实体。
[0010] 因此需要一套系统的基于侵入式组装方式，允许构件以主动的方式进行组合以满 足目标组装点的功能需求。无论是原子构件还是复合构件，其通过一种侵入（intrusion) 的方式强行插入到组装点。虽然，侵入式组装可以弥补传统构件组装的不足，但同样存在一 些问题：
[0011] 1)从实现细节的源代码级来看，侵入式组装将增加一些无用代码或危险代码；
[0012] 2)从组装高层的工作流来看，侵入式组装将附加一些无用的接口或威胁接口。
[0013] 针对这些组装问题，一方面需要保证构件交互的正确性，即对局部而言，交互接口 中的参数，参数顺序等是兼容的；另一方面需要保证组合的构件是安全性的，即对整体而 言，不存在隐藏的威胁，不存在违反既定的需求。而模型检验作为测试的辅助手段，是一种 自动化的、基于有限状态模型的性质验证方法，它通过显式的状态搜索或隐式的不动点计 算来检测系统模型是否满足预期性质，当模型不满足性质时输出反例信息，即模型中违背 性质的状态迹。基于此，将模型检验方法应用检验基于侵入式的灰盒组装方法组装的软件， 可以有效地验证构件组装过程的正确性和安全性，保证基于构件的软件系统的软件质量。
【发明内容】
[0014] 本发明的目的就是为了克服上述现有技术存在的缺陷而提供一种基于模型的侵 入式灰盒组装验证方法。
[0015] 本发明的目的可以通过以下技术方案来实现：
[0016] 一种基于模型的侵入式灰盒组装验证方法，包括步骤：
[0017] 1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模 型；
[0018] 2)实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中检 索，并确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位 置，若为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置；
[0019] 3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行 的Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。
[0020] 所述实例构件库的构建过程包括步骤：
[0021] A1 :将Java程序进行封装使其构件化，添加组装点，并采用反射技术解析出程序 功能的函数方法，以及组装点的接口信息；
[0022] A2 :根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参数名称， 参数类型和参数顺序。
[0023] A3 :将解析出的函数方法进行绑定，产生调用关系；
[0024] A4 :将构件化后的Java程序以XML形式保存，输出实例构件的封装文件；
[0025] A5 :将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封装文件 中标识其相关的应用领域，以提供构件组装时使用。
[0026] 所述步骤1)具体包括步骤：
[0027] 11)新建组装界面，根据待开发软件的业务逻辑绘制工作流；
[0028] 12)设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。
[0029] 13)在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止点。
[0030] 所述步骤2)中将单一实例构件插入至抽象构件所在位置的过程具体为：根据工 作流调用关系，绑定该实例构件与相邻抽象构件实例化得到的实例构件间的接口参数，包 括参数名称，参数类型，以及参数顺序。
[0031] 所述步骤2)中选择多个实例构件组合为复合构件并侵入至抽象构件所在位置的 过程中：
[0032] 以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件集合， 使得多个实例构件在组合后，既满足接口信息，又满足领域应用的要求；或
[0033] 以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得多 个实例构件在组合后，既满足接口信息，又满足领域应用的要求。
[0034] 所述步骤3)具体包括：
[0035] 31)根据实例化配置信息，输出相应的配置文件；
[0036] 32)转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本；
[0037] 33)检验组装构件是否满足正确性和安全性；
[0038] 34)通过执行模型检验器NuSMV对结构脚本执行检验，根据检验结果判断组装是 否满足正确性和安全性。
[0039] 所述步骤31)具体包括步骤：
[0040] 311)新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的名称 和功能；
[0041] 312)根据配置信息的接口定义部分，解析接口信息，并将解析得到的接口信息写 入该组装构件的接口定义部分；
[0042] 313)根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用于描述 构件调用关系，将调用关系写入该组装构件的工作流定义部分。
[0043] 314)使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关系，同 时标记组装点与下层构件之间的侵入关系。
[0044] 315)对配置文件进行语法检验，确保每个抽象构件都被实例化。
[0045] 所述步骤32)具体包括步骤：
[0046] 321)根据组装构件内部的实例构件的名称信息，得到转化的状态集；
[0047] 322)根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子命 题；
[0048] 323)根据工作流上的调用关系，转化为状态迀移关系；
[0049] 324)根据状态集、原子命题和状态迀移关系，构造Kripke结构的可验证脚本。< br>[0050] 325)对可验证脚本进行语法检验，确保组装语法是正确的。
[0051] 所述步骤33)具体包括步骤：
[0052] 331)从接口信息中接口参数覆盖准则出发，检验侵入式组装的正确性；
[0053] 332)检验组装构件是否有空接口没被使用；
[0054] 333)从功能迀移覆盖的角度出发，检验侵入式组装的安全性；
[0055] 334)检验组装构件是否有功能存在不可终止性。
[0056] 所述步骤34)具体为：
[0057] 通过执行模型检验器NuSMV对结构脚本执行检验，并根据检验结果判断构件组装 过程是否满足正确性和安全性，若为是，则将其配置文件输出并保存到构件库中，同时标记 组装构件的功能和应用领域属性，若为否，则执行提示错误信息。
[0058] 与现有技术相比，本发明具有以下优点：
[0059] 1)本发明在无法找到合适的单一实例构件时，采用将多个实例构件组合侵入至指 定位置，可以提高软件的开发效率，解决了抽象构件实例化时无法找到合适的单一构件的 问题。
[0060] 2)，应用模型检验技术检验构件组装的配置文件，此种采用模型检验方法可以实 现自动化检验灰盒组装正确性和安全性的目的。
[0061] 3)侵入过程以领域和功能作为基点，可以增加侵入过程的匹配度。
【附图说明】
[0062] 图1为本发明的侵入式灰盒组装验证流程图；
[0063] 图2为本发明的构件侵入方式表示图；
[0064] 图3为一个下层构件侵入上层构件的模型示例；
[0065] 图4为本发明的构件组装架构图；
[0066] 图5为本发明的构件配置文件结构图；
[0067] 图6为本发明的组装检验执行流程。
【具体实施方式】
[0068] 下面结合附图和具体实施例对本发明进行详细说明。本实施例以本发明技术方案 为前提进行实施，给出了详细的实施方式和具体的操作过程，但本发明的保护范围不限于 下述的实施例。
[0069] -种基于模型的侵入式灰盒组装验证方法，如图1所示，首先，采用反射技术针对 Java可执行程序进行解析，添加内部流程逻辑与组装点，并添加组装点，封装入构件库。其 次，用户根据需求在可视化界面设计抽象工作流。接着，针对工作流，在服务库中检索可满 足的单一实例构件。如果不存在满足的实例构件，则采用算法将多个实例构件按照一定的 组合方法侵入到组装点。抽象构件实例化的结果是得到组装配置文件。然后，转化配置文 件得到适合于模型检验器NuSMV执行的Kripke结构脚本。根据不同覆盖准则产生检验性 质，检验构件组装的正确性和安全性。最后，反馈用户检验结果。
[0070] 其中，实例构件库的构建过程包括步骤：
[0071] A1 :将Java程序进行封装使其实例构件化，添加组装点，并以.class为后缀名的 可执行代码采用反射技术解析出程序功能的函数方法，以及组装点的接口信息；
[0072] A2 :根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参数名称， 参数类型和参数顺序；
[0073] A3:在可视化图形编辑器上，将解析出的函数方法进行绑定，产生调用关系，具体 包括步骤：
[0074] A31 :在可视化编辑器上显示当前实例构件，用实线圆形图形元素表示函数方法。
[0075] A32 :拖动连接线绑定具有前后顺序关系的接口。
[0076] A33:添加其他图形元素描述该构件内部流程，用虚线圆形表示功能实体是内部不 可见的功能。
[0077] A34:若当前构件是可继续组装扩展的，则用菱形表示可待插入其他构件的组装 点。
[0078] A4 :将构件化后的Java程序以XML形式保存，并产生一个以.des为后缀的描述文 件作为实例构件封装文件；
[0079] A5 :将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封装文件 中标识其相关的应用领域，以提供构件组装时使用。
[0080] 具体的，组装验证方法包括步骤：
[0081] 1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模 型，具体包括步骤：
[0082] 11)新建组装界面，根据待开发软件的业务逻辑绘制工作流，具体为：在新建的组 装界面上，切换到工作流图形化编辑模式后，根据组装需求，拖动图形元素绘制组装的工作 流；
[0083] 12)设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。
[0084] 13)在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止点。
[0085] 14)以.wf为文件后缀名，保存工作流模型。
[0086] 2)实例化：根据工作流中各抽象构件的功能要求和接口信息在库中检索，并确认 是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位置，若为 否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置，具体包括步骤：
[0087] 21)切换到组装场景实例化功能界面，筛选实例构件，具体步骤如下：
[0088] 211)点击工作流上的抽象构件，从该构件抽象描述信息中读取构件需求描述；
[0089] 212)根据构件领域需求选取实例构件集合；
[0090] 213)根据构件功能描述筛选实例构件集合；
[0091] 214)根据数据参数个数，筛选满足参数个数的实例构件集合；
[0092] 215)根据数据参数类型，筛选满足参数类型的实例构件集合；
[0093] 216)根据数据参数顺序，筛选满足参数顺序的实例构件集合；
[0094] 217)执行步骤211)至步骤216)后，对实例构件集合中的构件进行排序。
[0095] 22)确认是否存在匹配的单一实例构件，若为是，则执行步骤23)，若为否，则执行 步骤 24);
[0096] 23)根据工作流调用关系，绑定该实例构件与相邻抽象构件实例化得到的构件间 的接口参数，包括参数名称，参数类型，以及参数顺序，具体步骤如下：
[0097] 231)在抽象构件的属性编辑区域，将该实例构件绑定到相应的抽象构件所在的图 形元素代表的组装点上；
[0098] 232)根据工作流调用关系，绑定构件间的接口参数，包括参数名称，参数类型，以 及参数顺序；
[0099] 233)点击保存实例化组装时，检查参数类型和参数顺序是否设置正确。
[0100] 24)以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件集 合，使得实例构件集合在一定的组合方式下，既满足接口信息，又满足领域应用的要求；或
[0101] 以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得实 例构件集合在一定的执行条件下，既满足接口信息，又满足领域应用的要求。
[0102] 图2给出了四种组合行为的侵入式组装方法。侵入的子构件可能不止一个，侵入 的形式也各有不同，这些子构件之间大致存在四种关系：选择，互斥，顺序，并发。选择和互 斥之间区别在于选择可以是若干个构件一起侵入，而互斥是有且仅有一个满足条件的构件 才能够侵入；顺序表不若干构件按顺序一个一个地侵入；并发关系表不若干子构件在同一 时间点一起侵入。图4中C表不主构件，If:^表不侵入的子构件。选择米用符号| |描 述，例如Ii111211…11in;互斥采用符号|描述，例如Ii112卜* | 序采用+描述，例如 Ii+I2+…+1心并发采用〈> 描述，例如IiOI'XMn)。
[0103] 图3描述了一个下层构件侵入上层构件的数据模型。从结构上分为两层：第一层 描述上层构件a，其存在一条％^路径，菱形区域q3表示人为设计的侵 入构件；第二层描述侵入的下层构件之间的关系，其选取的子构件b和C进行并发可实现组 装点q3的功能。从整体上看，b和c并发组合并以强制的方式侵入主构件a的组装点q3。
[0104]图4为本发明的构件组装架构图。椭圆形表示构件的接口，菱形表示侵入点，圆 形表示功能模块，箭头表示构件侵入组装方向。可视化层VisualApplication展示工作 流Workflow的流程；实例化层ConcretizationLevel组装实例构件；构件层Compone nt Level则描述构件功能；统一构件库UCR存储实例构件集。分层化地描述构件之间的关系， 形式化表达构件侵入与被侵入构件交互关联；底层为构件层，构件之间组合可通过构件侵 入方式组成框架。由若干个框架构成最终的可视化图形文件。接口支持各个构件间进行交 互。在构件内部流程中，预留了组装点用于构件侵入式组合，称为外联口。通过外联口体现 分层思想，表示在分层构件中，上层构件在被下层构件侵入时，下层侵入构件通过外联口中 参与上层构件的交互。主构件为最高层，底层的应用以侵入的方式层层插入构件中，因此越 底层包含的内容越细化。
[0105] 25)为组装点标识组装状态属性，具体步骤如下：
[0106] 251)为步骤23)完成的抽象构件实例化的节点，标识状态为插入点。
[0107] 252)为步骤24)完成的抽象构件实例化的节点，标识状态为侵入点，并将该节点 用菱形表示。
[0108] 253)如果步骤24)仍无法找到合适的实例构件（集），那么允许在组装点插入手 工编写的具体实现代码。
[0109] 26)如果插入组装点的实例构件还包含其它组装点，则返回执行步骤21)，使得组 装场景上的抽象构件以及组装点全部完成实例化操作。
[0110] 3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行 的Kripke结构脚本，并基于得带的结构脚本验证构件组装过程的正确性和安全性，具体包 括步骤：
[0111] 31)根据实例化配置信息，输出相应的配置文件，具体包括步骤：
[0112] 311)新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的名称 和功能；
[0113] 312)根据配置信息的接口定义部分，解析接口信息，并将这些信息写入该组装构 件的接口定义部分；
[0114] 313)根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用于描述 构件调用关系，将调用关系写入该组装构件的工作流定义部分；
[0115] 314)使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关系，同 时标记组装点与下层构件之间的侵入关系；
[0116] 315)对配置文件进行语法检验，确保每个抽象构件都被实例化。
[0117] 图5给出了一个描述构件的配置文件结构图，支持可视化灰盒组装过程涉及的构 件图形化框架的XML配置文件，用于描述构件输入/输出，以及侵入式组装验证。如下代码 所示，给出了构件的Schema模式。
[0118] 主要分为两个部分的定义，第一部分是关于构件接口的定义，第二部分是关于构 件工作流的定义。
[0120]
[0121]
[0122]
[0123] 在接口定义：
[0124] <xs:e1ementname= "Interface"type= "xs:string"maxOccurs ="unbounded" >??? </xs:element〉部分，以上XML文件对应的标签解释如表1所示：
[0125] 表 1 :
[0127] 在构件工作流的定义：
[0128] <xs:elementname=''Workflow"type="xs:string" >..?〈/xs:element〉部分， 以上XML文件对应的标签解释如表2所示：
[0129] 表 2
[0131]
[0132] 32)转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本，具体包 括步骤：
[0133] 321)根据组装构件内部的实例构件的名称信息，得到转化的状态集；
[0134] 322)根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子命 题；
[0135] 323)根据工作流上的调用关系，转化为状态迀移关系；
[0136] 324)根据状态集、原子命题和状态迀移关系，构造Kripke结构的可验证脚本；
[0137] 325)对可验证脚本进行语法检验，确保组装语法是正确的。
[0138] 33)检验组装构件是否满足正确性和安全性，具体包括步骤：
[0139] 331)从接口信息中接口参数覆盖准则出发，采用时态逻辑AG(p)性质检验侵入式 组装的正确性；
[0140] 332)采用命令deadlock检验组装构件是否有空接口没被使用；
[0141] 333)从功能迀移覆盖的角度出发，采用时态逻辑AF(p)性质检验侵入式组装的安 全性；
[0142] 334)采用命令livelock检验组装构件是否有功能存在不可终止性。
[0143] 34)通过执行模型检验器NuSMV对结构脚本执行检验，具体步骤如下：
[0144] 341)将Kripke结构的脚本输入到模型检验NuSMV中；
[0145] 342)输入33)步骤得到的用于检验的目标检验性质（集）是否可满足；
[0146] 342)执行模型检验器NuSMV，并查看执行结果。
[0147] 35)根据检验结果判断组装是否满足正确性和安全性具体为：通过执行模型检验 器NuSMV对结构脚本执行检验，并根据检验结果判断构件组装过程是否满足正确性和安全 性，若为是，则将其配置文件输出并保存到构件库中，同时标记组装构件的功能和应用领域 属性，若为否，则执行提示错误信息。
[0148]图6是本实施例组装检验执行流程。为了将配置文件转化为模型检验器所能接受 的可行执行文件，需要将配置文件进行解析并进行形式化建模和验证。具体步骤如下：
[0149]S1:形式化定义构件配置文件，映射XML标签使其可被机器所理解。具体步骤如 下：
[0150]S11:定义构件为五元组1C= (CN，FD，CD，I，W)，其中CN表示构件名称，FD描述构 件的功能，CD描述构件所属应用领域，I表示构件接口的集合，W表示构件内部流程行为的 集合。
[0151] 其中CN与XML标签Compoment_Name进行映射关联，FD与XML标签Functional Description进行映射关联，⑶与XML标签Compoment_Domain进行映射关联，I与XML标 签Interface进行映射关联，W与XML标签Workflow进行映射关联。
[0152] S12 :定义接口为三元组I= (IN,ID,IA)，其中IN表示接口名称，ID描述接口的功 能，IA描述接口属性集合。
[0153] 其中IN与XML标签Interface_Name进行映射关联，ID与XML标签Interface_ Description进行映射关联，IA与XML标签Interface_Attribute进行映射关联。
[0154] S13:定义接口属性为三远足IA=(AN，AT，ANU)，其中AN表示接口属性，ATG{St ring, Int, Char, Array, Float, Double, Boolean, Map, Byte}表不接口类型，ANU表不是否可 以为空。
[0155] 其中AN与XML标签Attribute_Name进行映射关联，AT与XML标签Attribute_ Type进行映射关联，ANU与XML标签Attribute_Nullable进行映射关联。
[0156] S14:定义构件内部流程为三元组W=(SN，ST，AT)，其中SN为流程状态名称， STG{Star,End,Inherent,Insert_Port,Intrusion_Port}为状态类型，AT是迁移关系集 合。
[0157] 其中SN与XML标签State_Name进行映射关联，ST与XML标签State_Type进行 映射关联，AT与XML标签Acti 〇n_T〇进行映射关联。
[0158]S15:定义迀移关系为二元组AT= (ATP,GC)，其中ATP是卫式条件，GC是状态名 称。
[0159] 其中 ATP 与 XML 标签 Action_Type 进行映射关联，GC 与 XML 标签 Guard_Condition 进tx映射关联。
[0160] S2:根据形式化定义，应用如下算法对配置文件进行解析，主要包括接口解析算法 和工作流解析算法，前者用户获得构件接口基本信息，后者用于解析 工作流得到符合模型 检验器语法规则的Kripke结构脚本。具体步骤如下：
[0161] S21 :根据如下算法解析构件接口。该算法以构件1C作为输入，输出构件接 口信息。其中，集合MapI N_表示保存的接口名字，针对接口参数进行解析，包括集合 MultiHashMaPlName表示保存多个接口参数名字，集合MultiHashMapAType表示保存多个接口 参数类型，集合MultiHashMapuun^表示保存多个接口参数是否可为空。
[0162]
[0163] S22 :定义目标转化形式化模型。为了实现模型检验，需要将组装配置文件转化为 状态迀移系统Kripke结构描述其行为M= (S，I，AP，L，T)，其中
[0164] 1、S是有限的状态集，每一个状态由组装中的构件与其卫式条件构成。
[0165] 2、I[S是初始状态集。
[0166] 3、AP是标记状态的原子命题，由接口状态类型决定。
[0167] 4、TgSxS是迁移关系集。
[0168] 5、L:S- 2AP是状态标记函数，L(s)表示状态s下所有为真的原子命题集。
[0169] S23 :根据如下算法解析构件工作流，使其转化为Kripke结构。对灰盒组装配置文 件进行解析构造相应的Kripke结构脚本。该算法以构件高层ICm作为输入，输出状态迀移 系统。其中，集合SN(w)和ST(w)解析工作流的名称和类型，并当接口不为空时迭代地解析 接口动作Action_To以构造迀移转化关系。
[0170]
[0172] S3:根据覆盖准则产生检验性质。具体步骤如下：
[0173] S31 :从接口参数覆盖准则出发，采用时态逻辑AG(p)性质检验侵入式组装的正确 性。
[0174] S32 :采用命令deadlock检验组装构件是否有空接口没被使用。
[0175] S33 :从功能迀移覆盖的角度出发，采用时态逻辑AF(p)性质检验侵入式组装的安 全性。
[0176] S34 :米用命令livelock检验组装构件是否有功能存在不可终止性。
[0177] S4 :将转化后的组装脚本和检验性质输入到模型检验NuSMV中，执行模型检验器 NuSMV。根据检验结果判断组装是否满足正确性和安全性。
【主权项】
1. 一种基于模型的侵入式灰盒组装验证方法，其特征在于，包括步骤： 1) 流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模型； 2) 实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中检索，并 确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位置，若 为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置； 3) 性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行的 Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。2. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述实例构件库的构建过程包括步骤： Al:将Java程序进行封装使其构件化，添加组装点，并采用反射技术解析出程序功能 的函数方法，以及组装点的接口信息； A2 :根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参数名称，参数 类型和参数顺序。 A3 :将解析出的函数方法进行绑定，产生调用关系； A4 :将构件化后的Java程序以XML形式保存，输出实例构件的封装文件； A5 :将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封装文件中标 识其相关的应用领域，以提供构件组装时使用。3. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤1)具体包括步骤： 11) 新建组装界面，根据待开发软件的业务逻辑绘制工作流； 12) 设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。 13) 在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止点。4. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤2)中将单一实例构件插入至抽象构件所在位置的过程具体为：根据工作流调用关 系，绑定该实例构件与相邻抽象构件实例化得到的实例构件间的接口参数，包括参数名称， 参数类型，以及参数顺序。5. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤2)中选择多个实例构件组合为复合构件并侵入至抽象构件所在位置的过程中： 以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件集合，使得 多个实例构件在组合后，既满足接口信息，又满足领域应用的要求；或 以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得多个实 例构件在组合后，既满足接口信息，又满足领域应用的要求。6. 根据权利要求3所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤3)具体包括： 31) 根据实例化配置信息，输出相应的配置文件； 32) 转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本； 33) 检验组装构件是否满足正确性和安全性； 34) 通过执行模型检验器NuSMV对结构脚本执行检验，根据检验结果判断组装是否满 足正确性和安全性。7. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤31)具体包括步骤： 311) 新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的名称和功 能； 312) 根据配置信息的接口定义部分，解析接口信息，并将解析得到的接口信息写入该 组装构件的接口定义部分； 313) 根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用于描述构件 调用关系，将调用关系写入该组装构件的工作流定义部分。 314) 使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关系，同时标 记组装点与下层构件之间的侵入关系。 315) 对配置文件进行语法检验，确保每个抽象构件都被实例化。8. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤32)具体包括步骤： 321) 根据组装构件内部实例构件的名称信息，得到转化的状态集； 322) 根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子命题； 323) 根据工作流上的调用关系，转化为状态迀移关系； 324) 根据状态集、原子命题和状态迀移关系，构造Kripke结构的可验证脚本； 325) 对可验证脚本进行语法检验，确保组装语法是正确的。9. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤33)具体包括步骤： 331) 从接口信息中接口参数覆盖准则出发，检验侵入式组装的正确性； 332) 检验组装构件是否有空接口没被使用； 333) 从功能迀移覆盖的角度出发，检验侵入式组装的安全性； 334) 检验组装构件是否有功能存在不可终止性。10. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤34)具体为： 通过执行模型检验器NuSMV对结构脚本执行检验，并根据检验结果判断构件组装过程 是否满足正确性和安全性，若为是，则将其配置文件输出并保存到构件库中，同时标记组装 构件的功能和应用领域属性，若为否，则执行提示错误信息。
【专利摘要】本发明涉及一种基于模型的侵入式灰盒组装验证方法，属于软件工程技术领域，包括步骤：1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模型；2)实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中检索，并确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位置，若为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置；3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行的Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。与现有技术相比，本发明具有提高基于构件的软件开发效率等优点。
【IPC分类】G06F11/36, G06F9/44
【公开号】CN104899037
【申请号】CN201510319556
【发明人】高洪皓, 陈颖, 田野, 曾红卫, 缪淮扣
【申请人】上海大学
【公开日】2015年9月9日
【申请日】2015年6月11日
【技术领域】
[0001] 本发明涉及一种软件工程技术，尤其是涉及一种基于模型的侵入式灰盒组装验证 方法。
【背景技术】
[0002] 基于构件的软件开发（Component-BasedSoftwareDevelopment,CBSD)是软件工 业化的大趋势。计算机软件构架由手工代码开发模式转变为重用可独立运行的、被封装的 构件模式，它具有更高的灵活性。由于复用算法和软件功能，基于构件的软件开发大大缩短 了软件系统的开发进度，尤其是在经费有限的情况下该方法是实现软件项目开发的最佳选 择。
[0003] 构件是将具有特定功能的模块或代码按照一定的格式进行封装。构件组装则是研 宄如何组装构件的机制，以需求模型为基础，查找合适的构件进行集成以快速开发系统软 件为目的。目前，构件组装技术主要分为黑盒组装方法，白盒组装方法和灰盒组装三种方 法。但各自存在优缺点：黑盒组装方法不需要对构件的实现细节有任何了解，也不需要对构 件进行配置或修改，但"以不变的构件组装成万变的应用"的理念过于现实化，实际应用难 度大。黑盒组装对功能进行抽象描述，使用户无法了解构件是如何运行的，缺乏对黑盒构件 的可信性。白盒组装方法则要求将构件的所有实现细节都展示出来，让复用者理解后再进 行组装，并可按应用需求对构件进行二次修改，但该方法需要用户对实现细节和具体需求 了如指掌，在程序可读性和可维护性方面存在应用的局限性。而灰盒组装方法介于黑盒和 白盒之间，其通过混合使用组装机制来架构系统软件实现用户组装需求，既灵活又高效。因 此，灰盒组装方法是目前构件组装技术的研宄重点和难点。
[0004] 在灰盒组装过程中，即要体现构件的部分实现细节，又要展示构件的部分模块功 能。实际上，构件组装的操作更加复杂，而且组装的正确性和安全性很难保证。涉及如下两 个主要问题：
[0005] 1)如何描述和表达灰盒组装的组装流程？包括展示部分实现细节和部分功能模 块。
[0006] 2)如何有效地对灰盒组装进行验证？包括构件组装的正确性和安全性。
[0007] 在传统的组装场景上，每个组装点的功能需求以push推的形式向构件库发出构 件检索请求，查询是否存在合适的构件，同时以pull拉的形式将目标实例构件插入到组装 点进行集成。这种方式目标明确，组合速度块。但在实际情况下，存在如下问题：
[0008] 1)由于缺少构件规格说明语言，很难正确地、形式化地描述push点的构件需求；
[0009] 2)由于构件库中的构件数量有限，很难准确地检索出满足请求的单个构件实体。
[0010] 因此需要一套系统的基于侵入式组装方式，允许构件以主动的方式进行组合以满 足目标组装点的功能需求。无论是原子构件还是复合构件，其通过一种侵入（intrusion) 的方式强行插入到组装点。虽然，侵入式组装可以弥补传统构件组装的不足，但同样存在一 些问题：
[0011] 1)从实现细节的源代码级来看，侵入式组装将增加一些无用代码或危险代码；
[0012] 2)从组装高层的工作流来看，侵入式组装将附加一些无用的接口或威胁接口。
[0013] 针对这些组装问题，一方面需要保证构件交互的正确性，即对局部而言，交互接口 中的参数，参数顺序等是兼容的；另一方面需要保证组合的构件是安全性的，即对整体而 言，不存在隐藏的威胁，不存在违反既定的需求。而模型检验作为测试的辅助手段，是一种 自动化的、基于有限状态模型的性质验证方法，它通过显式的状态搜索或隐式的不动点计 算来检测系统模型是否满足预期性质，当模型不满足性质时输出反例信息，即模型中违背 性质的状态迹。基于此，将模型检验方法应用检验基于侵入式的灰盒组装方法组装的软件， 可以有效地验证构件组装过程的正确性和安全性，保证基于构件的软件系统的软件质量。
【发明内容】
[0014] 本发明的目的就是为了克服上述现有技术存在的缺陷而提供一种基于模型的侵 入式灰盒组装验证方法。
[0015] 本发明的目的可以通过以下技术方案来实现：
[0016] 一种基于模型的侵入式灰盒组装验证方法，包括步骤：
[0017] 1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模 型；
[0018] 2)实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中检 索，并确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位 置，若为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置；
[0019] 3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行 的Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。
[0020] 所述实例构件库的构建过程包括步骤：
[0021] A1 :将Java程序进行封装使其构件化，添加组装点，并采用反射技术解析出程序 功能的函数方法，以及组装点的接口信息；
[0022] A2 :根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参数名称， 参数类型和参数顺序。
[0023] A3 :将解析出的函数方法进行绑定，产生调用关系；
[0024] A4 :将构件化后的Java程序以XML形式保存，输出实例构件的封装文件；
[0025] A5 :将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封装文件 中标识其相关的应用领域，以提供构件组装时使用。
[0026] 所述步骤1)具体包括步骤：
[0027] 11)新建组装界面，根据待开发软件的业务逻辑绘制工作流；
[0028] 12)设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。
[0029] 13)在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止点。
[0030] 所述步骤2)中将单一实例构件插入至抽象构件所在位置的过程具体为：根据工 作流调用关系，绑定该实例构件与相邻抽象构件实例化得到的实例构件间的接口参数，包 括参数名称，参数类型，以及参数顺序。
[0031] 所述步骤2)中选择多个实例构件组合为复合构件并侵入至抽象构件所在位置的 过程中：
[0032] 以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件集合， 使得多个实例构件在组合后，既满足接口信息，又满足领域应用的要求；或
[0033] 以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得多 个实例构件在组合后，既满足接口信息，又满足领域应用的要求。
[0034] 所述步骤3)具体包括：
[0035] 31)根据实例化配置信息，输出相应的配置文件；
[0036] 32)转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本；
[0037] 33)检验组装构件是否满足正确性和安全性；
[0038] 34)通过执行模型检验器NuSMV对结构脚本执行检验，根据检验结果判断组装是 否满足正确性和安全性。
[0039] 所述步骤31)具体包括步骤：
[0040] 311)新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的名称 和功能；
[0041] 312)根据配置信息的接口定义部分，解析接口信息，并将解析得到的接口信息写 入该组装构件的接口定义部分；
[0042] 313)根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用于描述 构件调用关系，将调用关系写入该组装构件的工作流定义部分。
[0043] 314)使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关系，同 时标记组装点与下层构件之间的侵入关系。
[0044] 315)对配置文件进行语法检验，确保每个抽象构件都被实例化。
[0045] 所述步骤32)具体包括步骤：
[0046] 321)根据组装构件内部的实例构件的名称信息，得到转化的状态集；
[0047] 322)根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子命 题；
[0048] 323)根据工作流上的调用关系，转化为状态迀移关系；
[0049] 324)根据状态集、原子命题和状态迀移关系，构造Kripke结构的可验证脚本。< br>[0050] 325)对可验证脚本进行语法检验，确保组装语法是正确的。
[0051] 所述步骤33)具体包括步骤：
[0052] 331)从接口信息中接口参数覆盖准则出发，检验侵入式组装的正确性；
[0053] 332)检验组装构件是否有空接口没被使用；
[0054] 333)从功能迀移覆盖的角度出发，检验侵入式组装的安全性；
[0055] 334)检验组装构件是否有功能存在不可终止性。
[0056] 所述步骤34)具体为：
[0057] 通过执行模型检验器NuSMV对结构脚本执行检验，并根据检验结果判断构件组装 过程是否满足正确性和安全性，若为是，则将其配置文件输出并保存到构件库中，同时标记 组装构件的功能和应用领域属性，若为否，则执行提示错误信息。
[0058] 与现有技术相比，本发明具有以下优点：
[0059] 1)本发明在无法找到合适的单一实例构件时，采用将多个实例构件组合侵入至指 定位置，可以提高软件的开发效率，解决了抽象构件实例化时无法找到合适的单一构件的 问题。
[0060] 2)，应用模型检验技术检验构件组装的配置文件，此种采用模型检验方法可以实 现自动化检验灰盒组装正确性和安全性的目的。
[0061] 3)侵入过程以领域和功能作为基点，可以增加侵入过程的匹配度。
【附图说明】
[0062] 图1为本发明的侵入式灰盒组装验证流程图；
[0063] 图2为本发明的构件侵入方式表示图；
[0064] 图3为一个下层构件侵入上层构件的模型示例；
[0065] 图4为本发明的构件组装架构图；
[0066] 图5为本发明的构件配置文件结构图；
[0067] 图6为本发明的组装检验执行流程。
【具体实施方式】
[0068] 下面结合附图和具体实施例对本发明进行详细说明。本实施例以本发明技术方案 为前提进行实施，给出了详细的实施方式和具体的操作过程，但本发明的保护范围不限于 下述的实施例。
[0069] -种基于模型的侵入式灰盒组装验证方法，如图1所示，首先，采用反射技术针对 Java可执行程序进行解析，添加内部流程逻辑与组装点，并添加组装点，封装入构件库。其 次，用户根据需求在可视化界面设计抽象工作流。接着，针对工作流，在服务库中检索可满 足的单一实例构件。如果不存在满足的实例构件，则采用算法将多个实例构件按照一定的 组合方法侵入到组装点。抽象构件实例化的结果是得到组装配置文件。然后，转化配置文 件得到适合于模型检验器NuSMV执行的Kripke结构脚本。根据不同覆盖准则产生检验性 质，检验构件组装的正确性和安全性。最后，反馈用户检验结果。
[0070] 其中，实例构件库的构建过程包括步骤：
[0071] A1 :将Java程序进行封装使其实例构件化，添加组装点，并以.class为后缀名的 可执行代码采用反射技术解析出程序功能的函数方法，以及组装点的接口信息；
[0072] A2 :根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参数名称， 参数类型和参数顺序；
[0073] A3:在可视化图形编辑器上，将解析出的函数方法进行绑定，产生调用关系，具体 包括步骤：
[0074] A31 :在可视化编辑器上显示当前实例构件，用实线圆形图形元素表示函数方法。
[0075] A32 :拖动连接线绑定具有前后顺序关系的接口。
[0076] A33:添加其他图形元素描述该构件内部流程，用虚线圆形表示功能实体是内部不 可见的功能。
[0077] A34:若当前构件是可继续组装扩展的，则用菱形表示可待插入其他构件的组装 点。
[0078] A4 :将构件化后的Java程序以XML形式保存，并产生一个以.des为后缀的描述文 件作为实例构件封装文件；
[0079] A5 :将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封装文件 中标识其相关的应用领域，以提供构件组装时使用。
[0080] 具体的，组装验证方法包括步骤：
[0081] 1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模 型，具体包括步骤：
[0082] 11)新建组装界面，根据待开发软件的业务逻辑绘制工作流，具体为：在新建的组 装界面上，切换到工作流图形化编辑模式后，根据组装需求，拖动图形元素绘制组装的工作 流；
[0083] 12)设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。
[0084] 13)在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止点。
[0085] 14)以.wf为文件后缀名，保存工作流模型。
[0086] 2)实例化：根据工作流中各抽象构件的功能要求和接口信息在库中检索，并确认 是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位置，若为 否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置，具体包括步骤：
[0087] 21)切换到组装场景实例化功能界面，筛选实例构件，具体步骤如下：
[0088] 211)点击工作流上的抽象构件，从该构件抽象描述信息中读取构件需求描述；
[0089] 212)根据构件领域需求选取实例构件集合；
[0090] 213)根据构件功能描述筛选实例构件集合；
[0091] 214)根据数据参数个数，筛选满足参数个数的实例构件集合；
[0092] 215)根据数据参数类型，筛选满足参数类型的实例构件集合；
[0093] 216)根据数据参数顺序，筛选满足参数顺序的实例构件集合；
[0094] 217)执行步骤211)至步骤216)后，对实例构件集合中的构件进行排序。
[0095] 22)确认是否存在匹配的单一实例构件，若为是，则执行步骤23)，若为否，则执行 步骤 24);
[0096] 23)根据工作流调用关系，绑定该实例构件与相邻抽象构件实例化得到的构件间 的接口参数，包括参数名称，参数类型，以及参数顺序，具体步骤如下：
[0097] 231)在抽象构件的属性编辑区域，将该实例构件绑定到相应的抽象构件所在的图 形元素代表的组装点上；
[0098] 232)根据工作流调用关系，绑定构件间的接口参数，包括参数名称，参数类型，以 及参数顺序；
[0099] 233)点击保存实例化组装时，检查参数类型和参数顺序是否设置正确。
[0100] 24)以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件集 合，使得实例构件集合在一定的组合方式下，既满足接口信息，又满足领域应用的要求；或
[0101] 以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得实 例构件集合在一定的执行条件下，既满足接口信息，又满足领域应用的要求。
[0102] 图2给出了四种组合行为的侵入式组装方法。侵入的子构件可能不止一个，侵入 的形式也各有不同，这些子构件之间大致存在四种关系：选择，互斥，顺序，并发。选择和互 斥之间区别在于选择可以是若干个构件一起侵入，而互斥是有且仅有一个满足条件的构件 才能够侵入；顺序表不若干构件按顺序一个一个地侵入；并发关系表不若干子构件在同一 时间点一起侵入。图4中C表不主构件，If:^表不侵入的子构件。选择米用符号| |描 述，例如Ii111211…11in;互斥采用符号|描述，例如Ii112卜* | 序采用+描述，例如 Ii+I2+…+1心并发采用〈> 描述，例如IiOI'XMn)。
[0103] 图3描述了一个下层构件侵入上层构件的数据模型。从结构上分为两层：第一层 描述上层构件a，其存在一条％^路径，菱形区域q3表示人为设计的侵 入构件；第二层描述侵入的下层构件之间的关系，其选取的子构件b和C进行并发可实现组 装点q3的功能。从整体上看，b和c并发组合并以强制的方式侵入主构件a的组装点q3。
[0104]图4为本发明的构件组装架构图。椭圆形表示构件的接口，菱形表示侵入点，圆 形表示功能模块，箭头表示构件侵入组装方向。可视化层VisualApplication展示工作 流Workflow的流程；实例化层ConcretizationLevel组装实例构件；构件层Compone nt Level则描述构件功能；统一构件库UCR存储实例构件集。分层化地描述构件之间的关系， 形式化表达构件侵入与被侵入构件交互关联；底层为构件层，构件之间组合可通过构件侵 入方式组成框架。由若干个框架构成最终的可视化图形文件。接口支持各个构件间进行交 互。在构件内部流程中，预留了组装点用于构件侵入式组合，称为外联口。通过外联口体现 分层思想，表示在分层构件中，上层构件在被下层构件侵入时，下层侵入构件通过外联口中 参与上层构件的交互。主构件为最高层，底层的应用以侵入的方式层层插入构件中，因此越 底层包含的内容越细化。
[0105] 25)为组装点标识组装状态属性，具体步骤如下：
[0106] 251)为步骤23)完成的抽象构件实例化的节点，标识状态为插入点。
[0107] 252)为步骤24)完成的抽象构件实例化的节点，标识状态为侵入点，并将该节点 用菱形表示。
[0108] 253)如果步骤24)仍无法找到合适的实例构件（集），那么允许在组装点插入手 工编写的具体实现代码。
[0109] 26)如果插入组装点的实例构件还包含其它组装点，则返回执行步骤21)，使得组 装场景上的抽象构件以及组装点全部完成实例化操作。
[0110] 3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行 的Kripke结构脚本，并基于得带的结构脚本验证构件组装过程的正确性和安全性，具体包 括步骤：
[0111] 31)根据实例化配置信息，输出相应的配置文件，具体包括步骤：
[0112] 311)新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的名称 和功能；
[0113] 312)根据配置信息的接口定义部分，解析接口信息，并将这些信息写入该组装构 件的接口定义部分；
[0114] 313)根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用于描述 构件调用关系，将调用关系写入该组装构件的工作流定义部分；
[0115] 314)使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关系，同 时标记组装点与下层构件之间的侵入关系；
[0116] 315)对配置文件进行语法检验，确保每个抽象构件都被实例化。
[0117] 图5给出了一个描述构件的配置文件结构图，支持可视化灰盒组装过程涉及的构 件图形化框架的XML配置文件，用于描述构件输入/输出，以及侵入式组装验证。如下代码 所示，给出了构件的Schema模式。
[0118] 主要分为两个部分的定义，第一部分是关于构件接口的定义，第二部分是关于构 件工作流的定义。
[0120]
[0121]
[0122]
[0123] 在接口定义：
[0124] <xs:e1ementname= "Interface"type= "xs:string"maxOccurs ="unbounded" >??? </xs:element〉部分，以上XML文件对应的标签解释如表1所示：
[0125] 表 1 :
[0127] 在构件工作流的定义：
[0128] <xs:elementname=''Workflow"type="xs:string" >..?〈/xs:element〉部分， 以上XML文件对应的标签解释如表2所示：
[0129] 表 2
[0131]
[0132] 32)转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本，具体包 括步骤：
[0133] 321)根据组装构件内部的实例构件的名称信息，得到转化的状态集；
[0134] 322)根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子命 题；
[0135] 323)根据工作流上的调用关系，转化为状态迀移关系；
[0136] 324)根据状态集、原子命题和状态迀移关系，构造Kripke结构的可验证脚本；
[0137] 325)对可验证脚本进行语法检验，确保组装语法是正确的。
[0138] 33)检验组装构件是否满足正确性和安全性，具体包括步骤：
[0139] 331)从接口信息中接口参数覆盖准则出发，采用时态逻辑AG(p)性质检验侵入式 组装的正确性；
[0140] 332)采用命令deadlock检验组装构件是否有空接口没被使用；
[0141] 333)从功能迀移覆盖的角度出发，采用时态逻辑AF(p)性质检验侵入式组装的安 全性；
[0142] 334)采用命令livelock检验组装构件是否有功能存在不可终止性。
[0143] 34)通过执行模型检验器NuSMV对结构脚本执行检验，具体步骤如下：
[0144] 341)将Kripke结构的脚本输入到模型检验NuSMV中；
[0145] 342)输入33)步骤得到的用于检验的目标检验性质（集）是否可满足；
[0146] 342)执行模型检验器NuSMV，并查看执行结果。
[0147] 35)根据检验结果判断组装是否满足正确性和安全性具体为：通过执行模型检验 器NuSMV对结构脚本执行检验，并根据检验结果判断构件组装过程是否满足正确性和安全 性，若为是，则将其配置文件输出并保存到构件库中，同时标记组装构件的功能和应用领域 属性，若为否，则执行提示错误信息。
[0148]图6是本实施例组装检验执行流程。为了将配置文件转化为模型检验器所能接受 的可行执行文件，需要将配置文件进行解析并进行形式化建模和验证。具体步骤如下：
[0149]S1:形式化定义构件配置文件，映射XML标签使其可被机器所理解。具体步骤如 下：
[0150]S11:定义构件为五元组1C= (CN，FD，CD，I，W)，其中CN表示构件名称，FD描述构 件的功能，CD描述构件所属应用领域，I表示构件接口的集合，W表示构件内部流程行为的 集合。
[0151] 其中CN与XML标签Compoment_Name进行映射关联，FD与XML标签Functional Description进行映射关联，⑶与XML标签Compoment_Domain进行映射关联，I与XML标 签Interface进行映射关联，W与XML标签Workflow进行映射关联。
[0152] S12 :定义接口为三元组I= (IN,ID,IA)，其中IN表示接口名称，ID描述接口的功 能，IA描述接口属性集合。
[0153] 其中IN与XML标签Interface_Name进行映射关联，ID与XML标签Interface_ Description进行映射关联，IA与XML标签Interface_Attribute进行映射关联。
[0154] S13:定义接口属性为三远足IA=(AN，AT，ANU)，其中AN表示接口属性，ATG{St ring, Int, Char, Array, Float, Double, Boolean, Map, Byte}表不接口类型，ANU表不是否可 以为空。
[0155] 其中AN与XML标签Attribute_Name进行映射关联，AT与XML标签Attribute_ Type进行映射关联，ANU与XML标签Attribute_Nullable进行映射关联。
[0156] S14:定义构件内部流程为三元组W=(SN，ST，AT)，其中SN为流程状态名称， STG{Star,End,Inherent,Insert_Port,Intrusion_Port}为状态类型，AT是迁移关系集 合。
[0157] 其中SN与XML标签State_Name进行映射关联，ST与XML标签State_Type进行 映射关联，AT与XML标签Acti 〇n_T〇进行映射关联。
[0158]S15:定义迀移关系为二元组AT= (ATP,GC)，其中ATP是卫式条件，GC是状态名 称。
[0159] 其中 ATP 与 XML 标签 Action_Type 进行映射关联，GC 与 XML 标签 Guard_Condition 进tx映射关联。
[0160] S2:根据形式化定义，应用如下算法对配置文件进行解析，主要包括接口解析算法 和工作流解析算法，前者用户获得构件接口基本信息，后者用于解析 工作流得到符合模型 检验器语法规则的Kripke结构脚本。具体步骤如下：
[0161] S21 :根据如下算法解析构件接口。该算法以构件1C作为输入，输出构件接 口信息。其中，集合MapI N_表示保存的接口名字，针对接口参数进行解析，包括集合 MultiHashMaPlName表示保存多个接口参数名字，集合MultiHashMapAType表示保存多个接口 参数类型，集合MultiHashMapuun^表示保存多个接口参数是否可为空。
[0162]
[0163] S22 :定义目标转化形式化模型。为了实现模型检验，需要将组装配置文件转化为 状态迀移系统Kripke结构描述其行为M= (S，I，AP，L，T)，其中
[0164] 1、S是有限的状态集，每一个状态由组装中的构件与其卫式条件构成。
[0165] 2、I[S是初始状态集。
[0166] 3、AP是标记状态的原子命题，由接口状态类型决定。
[0167] 4、TgSxS是迁移关系集。
[0168] 5、L:S- 2AP是状态标记函数，L(s)表示状态s下所有为真的原子命题集。
[0169] S23 :根据如下算法解析构件工作流，使其转化为Kripke结构。对灰盒组装配置文 件进行解析构造相应的Kripke结构脚本。该算法以构件高层ICm作为输入，输出状态迀移 系统。其中，集合SN(w)和ST(w)解析工作流的名称和类型，并当接口不为空时迭代地解析 接口动作Action_To以构造迀移转化关系。
[0170]
[0172] S3:根据覆盖准则产生检验性质。具体步骤如下：
[0173] S31 :从接口参数覆盖准则出发，采用时态逻辑AG(p)性质检验侵入式组装的正确 性。
[0174] S32 :采用命令deadlock检验组装构件是否有空接口没被使用。
[0175] S33 :从功能迀移覆盖的角度出发，采用时态逻辑AF(p)性质检验侵入式组装的安 全性。
[0176] S34 :米用命令livelock检验组装构件是否有功能存在不可终止性。
[0177] S4 :将转化后的组装脚本和检验性质输入到模型检验NuSMV中，执行模型检验器 NuSMV。根据检验结果判断组装是否满足正确性和安全性。
【主权项】
1. 一种基于模型的侵入式灰盒组装验证方法，其特征在于，包括步骤： 1) 流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模型； 2) 实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中检索，并 确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位置，若 为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置； 3) 性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行的 Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。2. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述实例构件库的构建过程包括步骤： Al:将Java程序进行封装使其构件化，添加组装点，并采用反射技术解析出程序功能 的函数方法，以及组装点的接口信息； A2 :根据反射出来的接口信息，确认接口以及接口参数，包括参数个数，参数名称，参数 类型和参数顺序。 A3 :将解析出的函数方法进行绑定，产生调用关系； A4 :将构件化后的Java程序以XML形式保存，输出实例构件的封装文件； A5 :将实例构件保存到实例构件库中，建立实例构件的索引信息，同时在封装文件中标 识其相关的应用领域，以提供构件组装时使用。3. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤1)具体包括步骤： 11) 新建组装界面，根据待开发软件的业务逻辑绘制工作流； 12) 设计工作流上抽象构件，并描述抽象构件的接口信息和功能要求。 13) 在工作流上，标识抽象构件的构件状态，包括初始点，中间点，以及终止点。4. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤2)中将单一实例构件插入至抽象构件所在位置的过程具体为：根据工作流调用关 系，绑定该实例构件与相邻抽象构件实例化得到的实例构件间的接口参数，包括参数名称， 参数类型，以及参数顺序。5. 根据权利要求1所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤2)中选择多个实例构件组合为复合构件并侵入至抽象构件所在位置的过程中： 以领域优先原则，采用启发式随机算法给出满足当前抽象构件的实例构件集合，使得 多个实例构件在组合后，既满足接口信息，又满足领域应用的要求；或 以功能优先原则，采用相似度计算方法给出多个跨领域的实例构件集合，使得多个实 例构件在组合后，既满足接口信息，又满足领域应用的要求。6. 根据权利要求3所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤3)具体包括： 31) 根据实例化配置信息，输出相应的配置文件； 32) 转化配置文件，产生可用于模型检验器NuSMV执行的Kripke结构脚本； 33) 检验组装构件是否满足正确性和安全性； 34) 通过执行模型检验器NuSMV对结构脚本执行检验，根据检验结果判断组装是否满 足正确性和安全性。7. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤31)具体包括步骤： 311) 新建一个配置文件，在其中写入配置信息的版本号，并描述组装构件的名称和功 能； 312) 根据配置信息的接口定义部分，解析接口信息，并将解析得到的接口信息写入该 组装构件的接口定义部分； 313) 根据工作流上的顺序关系，并发关系，互斥顺序和选择关系，解析并用于描述构件 调用关系，将调用关系写入该组装构件的工作流定义部分。 314) 使用深度搜索方式对每层的侵入式构件进行标记以区别构件之间的关系，同时标 记组装点与下层构件之间的侵入关系。 315) 对配置文件进行语法检验，确保每个抽象构件都被实例化。8. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤32)具体包括步骤： 321) 根据组装构件内部实例构件的名称信息，得到转化的状态集； 322) 根据实例构件状态，以及接口信息中的参数信息，得到实例构件的原子命题； 323) 根据工作流上的调用关系，转化为状态迀移关系； 324) 根据状态集、原子命题和状态迀移关系，构造Kripke结构的可验证脚本； 325) 对可验证脚本进行语法检验，确保组装语法是正确的。9. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤33)具体包括步骤： 331) 从接口信息中接口参数覆盖准则出发，检验侵入式组装的正确性； 332) 检验组装构件是否有空接口没被使用； 333) 从功能迀移覆盖的角度出发，检验侵入式组装的安全性； 334) 检验组装构件是否有功能存在不可终止性。10. 根据权利要求6所述的一种基于模型的侵入式灰盒组装验证方法，其特征在于，所 述步骤34)具体为： 通过执行模型检验器NuSMV对结构脚本执行检验，并根据检验结果判断构件组装过程 是否满足正确性和安全性，若为是，则将其配置文件输出并保存到构件库中，同时标记组装 构件的功能和应用领域属性，若为否，则执行提示错误信息。
【专利摘要】本发明涉及一种基于模型的侵入式灰盒组装验证方法，属于软件工程技术领域，包括步骤：1)流程设计：根据待开发软件的业务逻辑，设计由多个抽象构件构成的工作流模型；2)实例化：根据工作流中各抽象构件的功能要求和接口信息在实例构件库中检索，并确认是否存在匹配的单一实例构件，若为是，则将该实例构件插入至抽象构件所在位置，若为否，则选择多个实例构件组合为复合构件并侵入至抽象构件所在位置；3)性质验证：转化实例化所产生的配置文件，得到适合于模型检验器NuSMV执行的Kripke结构脚本，并基于该脚本验证构件组装过程的正确性和安全性。与现有技术相比，本发明具有提高基于构件的软件开发效率等优点。
【IPC分类】G06F11/36, G06F9/44
【公开号】CN104899037
【申请号】CN201510319556
【发明人】高洪皓, 陈颖, 田野, 曾红卫, 缪淮扣
【申请人】上海大学
【公开日】2015年9月9日
【申请日】2015年6月11日
最新回复(0)