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

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描述该服务层模型的部分代码为： 　　 　　 　　 　　 　　to variable=TavelRequest 　　part=TavelTypeInfo/ 　　 　　invoke partnerLink=Tavel 　　portType=tns：TavelPT 　　operation=requestTavel 　　inputVariable=TavelRequest 　　outputVariable=TavelInfo 　　 　　 　　receive partnerLink=Tavel portType=tns：TavelCallbackPT 　　operation=sendTavel 　　variable=DateInfo/ 　　 　　2 BPEL模型的Promela语言建模 　　Promela语言一种形式化语言，实现了对有限状态系统的建模。Pro