一种增强SOA可生存性的降级服务替换验证方法

摘要

本发明属于SOA技术领域,具体为增强SOA可生存性的降级服务替换验证方法。主要步骤：1.采用进程代数形式化建模WS-BPEL描述文件所体现的组合服务交互协议,包括：服务契约，成员服务可允许的消息交互；2.流程决策点，分析流程形式服务的消息操作（即发送、接受消息）选择。采用白盒策略描述WS-BPEL流程形式的替换服务和候选服务、以及服务组合和替换的上下文环境。3.将服务替换准则确定为服务相容性被定义为组合系统的可执行完成属性。在此基础上，4.验证实施替换后不影响系统相容性的降级服务替换，以及实施替换后的降级系统是否满足用户需求。本发明解决了现有技术无法验证降级服务替换正确性的问题。

主权项

一种增强SOA可生存性的降级服务替换验证方法，其特征在于具体步骤为：步骤一、采用进程代数形式化建模WS‑BPEL描述文件所体现的组合服务交互协议利用进程代数这一形式化工具对服务及其组合环境进行形式化建模，其中，成员服务及组合服务的系统模型表示为服务契约；所述服务契约用以描述服务外部可观测的消息行为；由于WS‑BPEL提供了参与组合的服务集合、服务的调用关系和消息的往来信息，这里采用白盒策略描述WS‑BPEL流程形式的替换服务和候选服务以及服务组合和替换的上下文环境；采用演算描述一个WS‑BPEL流程服务即服务契约C，具体语法如下：这里，表示流程服务的一个接口，表示发送消息操作，即沿接口发出消息；表示接收消息操作，即沿接口接收消息；表示没有消息交互的内部操作；根据服务契约的操作语义规则，表示服务契约执行操作后演化为，表示隐藏操作， 意味着在中的消息操作变为，即，当多个服务组合成一个服务系统时，某些服务仅提供部分接口，并且某些接口及其相关消息操作变成了内部不可观察的；步骤二、建立流程决策点，分析WS‑BPEL流程形式服务的消息交互行为在WS‑BPEL流程服务交互环境中，区分三类服务契约的决策点：（1）仅有发送消息操作的决策点； （2）仅有接受消息操作的决策点；（3）同时包括发送消息操作和接受消息操作的决策点；其中，第三类流程决策点是指同一服务接口的发送消息操作和接受消息操作；步骤三、建立服务替换正确性准则，定义服务相容性包括两大部分：其一，是在所有计算路径上完成属性；其二，在部分计算路径上的“测试成功”；设一组WS‑BPEL流程服务组合，记为系统；系统满足完成相容属性，记为，如果下列条件之一成立：(1) 如果是自包含系统，对于任意以致，；(2) 如果是开放系统，对于任意以致，存在以致；步骤四、降级服务替换正确性验证包括两部分：其一,服务子契约以较原契约更少的可交换消息集保持了所有计算路径上的服务相容性；其二,服务契约的测试精化，在部分计算路径上保持了服务相容性；一个WS‑BPEL流程服务契约是另一服务契约的子契约，记为，如果下列条件成立：（1）如果是一个决策点即顶层操作是一个选择，那么也是一个和具有相同类型的决策点；（2）对于每个接收消息操作以致，存在以致；（3）对于每个发送消息操作以致,存在,以致；如果，WS‑BPEL流程服务契约是的子契约，那么，对于相同的运行环境，替换后不改变系统原有的完成属性,即：如果，那么，；在使用子契约实施替换后，一个系统仍保持系统原有的相容性；然而，由于使用子契约实施的替换是不等价替换，所以，系统的某些服务行为会受到影响，这个影响分为两方面：第一，如果子契约提供了更多的消息接收能力，并且具有相同的发送消息非决定性选择，那么，这个替换不影响系统的运行，并且系统将具有更多的服务能力；第二，如果子契约提供了更多的消息接收能力，但是发送消息的非决定性选择减少，即发送更少的消息，那么，替换会对系统的全局行为产生两个方面的影响，即：（1）较原契约更少的消息交换集合；（2）较原契约更少的可完成计算路径；最后，实现增强SOA系统可生存性的降级服务替换；这里，用保留的服务契约来描述降级服务替换后用户期望保留的系统功能，记为；其中，是WS‑BPEL流程服务系统；依据正确服务替换的要求，实施服务替换后必须满足；令，其中，是WS‑BPEL流程服务契约，且,；对于任意，如果下列条件成立：(1)；(2) 对于每个消息发送操作以致,在中也存在。