RGPS服务层元模型正确性验证

张莉+杨淑贞+杨浩

摘 要：随着网络式软件复杂程度的日益增加，如何确保网络式软件功能和性能的正确性越发重要。根据网络式软件的特点，在RGPS需求元建模框架的指导下，提出RGPS服务层元模型正确性验证。首先用BPEL语言和WSDL语言把RGPS服务层元模型描述成BPEL模型，再用Promela语言实现BPEL模型的建模，最后输入LTL公式对RGPS服务层元模型进行安全性和活性验证分析。以城市交通出行系统为例，采用RGPS需求元模型为框架，构建城市交通出行系统服务层元模型。

关键词：网络式软件；BPEL；Promela；LTL公式；正确性验证

DOIDOI：10.11907/rjdk.162588

中图分类号：TP306

文献标识码：A文章编号：1672-7800（2016）012-0008-03

0 引言

随着计算机网络的迅速发展，计算机软件也朝着网络化、服务化方向转变，网络式软件[1-3]就是在这种形势下产生的一种复杂软件系统。网络式软件将网络资源聚合部署到网络上，为用户提供随个人需求而变化的在线服务。RGPS需求元模型框架是一种由分层与合作问题组成的框架，它涵盖了网络式软件描述中所需的角色、目标、流程和服务4个基本要素，由角色层元模型、目标层元模型、过程层元模型和服务层元模型以及各层之间相互关系组成。角色层元模型定义了需求方和需求方的社会属性、所需要承担的角色、所属的组织、规则以及相互之间的关系。目标层元模型将需求目标进行分类，确定各个目标之间的分解和约束关系。过程层元模型描述需求过程的各个组成部分，包括过程的输入、输出、前置条件、后置条件、组合过程中子流程之间的控制结构等。服务层元模型描述了服务信息以及它们的相互关系，用来指导服务链的构造及其所需服务资源的管理。

模型检测技术[4-6]是一种很重要的形式化验证分析技术。它最早由Clarke和Emerson于1981年提出，能通过显式的状态搜索或隐式不动点计算来验证系统是否满足某种属性或者实现某个功能。有形枚举的模型检测方法通过对状态的搜索遍历，找到所有的可达集，再检查可达集中是否存在错误状态。如果存在错误状态，那么说明系统不安全，否则说明系统是安全的。SPIN是一种常见的有形枚举的模型检测工具。

本文首先采用BPEL语言和WSDL语言把RGPS服务层元模型描述成BPEL模型，再对BPEL模型进行Promela语言建模，最后对RGPS服务层元模型进行验证分析。

1 RGPS服务层元模型的BPEL模型

服务可以分为原子服务和组合服务两种。组合服务是原子服务按照一定的过程控制结构组合编排而成。消息和操作是服务的两个基本要素。消息是服务所需的数据，分为输入消息和输出消息。操作分为前置条件和效果。服务描述分为功能性描述和非功能性描述。功能性描述介绍服务的主要业务。非功能性描述分为质量属性和情境属性，包括时间、费用和可维护性等。

BPEL是业务流程执行语言，用于描述业务流程的结构，调用网络服务，进行流程中数据的定义和传递。WSDL是网络服务描述语言，BPEL定义的流程都要通过WSDL来实现，并且被调用的网络服务也是用WSDL描述的。

随着城市交通系统的发展，城市交通系统网络也变得愈加复杂。本文以城市交通出行系统为例子，采用RGPS需求元模型为框架，构建城市交通出行系统服务层元模型。

图1中，当收到出行者的查询动作后，流程初始化3个并行的任务：计算出行价格、选择车次和路线以及为出行安排日期。虽然有些处理可以并行进行，但是3个任务之间存在相互依赖的控制和数据。具体地说，在计算最终价格时需要车次和路线信息，在全面安排实现计划时需要出行日期。在完成这3个任务后就可以将出行计划交给出行者。

用BPEL描述该服务层模型的部分代码为：

part="TavelTypeInfo"/>

portType="tns：TavelPT"

operation="requestTavel"

inputVariable="TavelRequest">

outputVariable="TavelInfo">

operation="sendTavel"

variable="DateInfo"/>

2 BPEL模型的Promela语言建模

Promela语言一种形式化语言，实现了对有限状态系统的建模。Promela描述的行为通过通道实现进程间通信和数据交换。一般来说，Promela模型由类型、通道、变量和进程构成。Promela语言主要有数据类型、进程、消息传递、控制流、语句类型。通过用JAVA编写程序代码，得到BPEL模型的Promela语言建模主程序代码：

if （e.getSource（） == menuItembpel2）

{

final String testBpelFile =bpelfileName；

final String testWsdlFile = wsdlfileName；

final String inputStreamFile = promelafileName；

try {

TestTranslator.translator（testBpelFile，testWsdlFile，new PrintStream（inputStreamFile））；

promelafile = new File（inputStreamFile）；

editorArea.setText（editor.readFile（promelafile））；

}catch （FileNotFoundException e1） {

// TODO Auto-generated catch block

e1.printStackTrace（）；

} catch （IOException e2） {

// TODO Auto-generated catch block

e2.printStackTrace（）；

}

城市交通出行系统的Promela语言部分代码为：

typedef T_BPEL_lc_basic {

byte state = BPEL_lc_basic_state_not_started；

}；

typedef T_BPEL_lc{

byte state = BPEL_lc_state_not_started；

bit fault = BPEL_lc_fault_none；

bit fault_handler = BPEL_lc_fault_handler_none；

}；

typedef T_BPEL_lnk {

bool evaluated = 0；

bool evaluation = 0；

}；

3 正确性验证

BPEL模型经过Promela语言建模之后，需要在SPIN工具输入LTL公式进行正确性验证，而正确性验证又分为安全性验证和活性验证。

SPIN工具是由美国贝尔实验室开发的用来验证大规模复杂软件系统的形式化验证工具。SPIN工具以Promela语言作为输入语言，使用on-the-fly技术，可以看作一个完整的LTL模型检测系统，里面有多项可供选择的优化技术。LTL公式即线性时序逻辑公式，LTL包括&&，！，―>，‖等连接符和□，◇，○等时序算子。□p表示p永远为真，◇p表示p在未来某一时刻为真，○p表示在下一时刻为真，pq表示p一直为真直到q为真。安全性是指坏的事情永远不会发生，活性是指好的事情最终会发生。

本文开发出了RGPS服务层元模型正确性验证工具，该工具用Java语言编程实现。用户首先用BPEL语言把RGPS服务层元模型例子给描述出来，再通过编写代码实现BPEL语言和Promela语言之间的转换生成Promela语言建模，接着用LTL公式描述模型的性质，最后进行SPIN验证返回检测结果。

LTL公式！[]（p1->！p2）的意思是由初始价格得不到最终价格的情况不会发生。输入LTL公式！[]（p1->！p2）进行安全性验证得到如下结果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

cycle checks-（disabled by –DSAFETY）

invalid end states +（disabled by never claim）

State-vector 121 byte， depth reached 142， errors： 0

验证结果显示没有错误发生，表明此公式成立。

LTL公式[]p的意思是无论什么情况下，系统都没有坏的事情发生。输入LTL公式[]p进行安全性验证得到如下结果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

cycle checks –（disabled by –DSAFETY）

invalid end states –（disabled by never claim）

State-vector38 byte， depth reached 172， errors： 1

验证结果显示有错误发生，表明此公式成立。

LTL公式[]（p1&&t1-><>p2）的意思是由初始价格和乘车信息就一定能得到最终价格。输入LTL公式[]（p1&&t1-><>p2）进行活性验证得到如下结果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

acceptance cycles –（fairness enabled）

invalid end states +（disabled by never claim）

State-vector 55 byte， depth reached 138， errors： 0

验证结果显示没有错误发生，表明此公式成立。

LTL公式[]<>p&&[]<>w的意思是在乘车信息未知的情况下能得到票价或者出行日期。输入LTL公式[]<>p&&[]<>w进行活性验证得到如下结果：

Full statespace search for：

never claim –

assertion violations +（if within scope of claim）

acceptance cycles –（fairness enabled）

invalid end states –（disabled by never claim）

State-vector 97 byte， depth reached 122， errors： 1

验证结果显示有错误发生，表明此公式成立。

4 结语

随着Internet技术的发展和软件生成运行环境的变化，网络式软件成为基于互联网环境的新生软件形态。为了克服网络式软件复杂度过高和缓解模型检测所引发的空间状态爆炸问题，本文研究了基于Promela模型组合与抽象的分析方法对RGPS服务层元模型进行正确性验证。RGPS服务层元模型正确性验证采用技术研究与工具开发相结合的方式。一方面，对核心技术进行长期系统深入研究，特别是实现BPEL/WSDL语言转换到Promela语言， 并结合LTL公式性质进行安全性和活性验证；另一方面，将理论研究上的突破转化到实践开发工具中，顺应国内外软件验证需求的潮流。

参考文献：

[1] 胡博，何克清，陈华峰.基于RGPS的网络式软件需求获取与分析方法[J].微计算机信息，2010，26（2）：6-8.

[2] 赵新辉，袁开银，吴尽昭.网络式软件非功能需求冲突消解[J].计算机工程，2012，38（18）：37-41.

[3] 张婷.网络式软件非功能需求分析方法及其应用[J].信息与电脑，2014，06：160-161.

[4] 林惠民，张文辉.模型检测：理论、方法与应用[J].电子学报，2002，30（12A）：1907-1912.

[5] 骆翔宇，谭征，苏开乐，吴立军.一种基于认知模型检测的Web服务组合验证方法[J].计算机学报，2011，34（6）：1041-1061

[6] 文中华，黄巍，刘任任，姜云飞.模型检测规划中的状态分层方法[J].软件学报，2009，20（4）：858-869.

[7] 张曼，段振华，王小兵.BPEL流程建模中的交叠模式分析与转换[J].软件学报，2011，22（11）：2684-2697.

[8] 张文博，史维峰.基于BPEL和QoS的动态Web服务组合框架研究[J].计算机技术与发展，2009，19（11）：72-75.

（责任编辑：陈福时）