法律状态公告日
法律状态信息
法律状态
2020-04-17
未缴年费专利权终止 IPC(主分类):G06F11/36 授权公告日:20120530 终止日期:20190504 申请日:20100504
专利权的终止
2012-05-30
授权
授权
2010-11-03
实质审查的生效 IPC(主分类):G06F11/36 申请日:20100504
实质审查的生效
2010-09-15
公开
公开
技术领域
本发明涉及服务计算中服务接口的验证方法,尤其是具备长事务特征服务接口的验证方法。
背景技术
Internet给人们的生活带来了巨大的影响,它改变着人们生产、工作、生活和学习的方式,是社会和经济发展的重要推动力。在Internet环境下,由于网络的分布、动态、和异构等特点,使Internet上的软件面临的环境从静态封闭逐步走向开放、动态和多变,软件系统为了适应这样一种发展趋势,将会逐步呈现出柔性、多目标、连续反应等多种形态。面对这种新型的软件形态,传统的软件理论、方法、技术和平台面临一系列挑战。在此背景下,人们开始探索新的软件技术,面向服务计算(Service-Oriented Computing,简称SOC)这种新的计算范型被提出。SOC中使用服务作为构建软件系统的基本元素,在系统交互层面体现为面向服务的体系结构(Service-Oriented Architecture,简称SOA)。
服务接口是SOC中关于某个服务所能够得到的唯一信息,一个服务接口代表了一个服务,其中说明了服务该如何使用、服务所能够提供的保证以及使用服务的前提或代价等方面的信息。准确而且充分的服务接口是保证SOC中服务查找、组合、调用等关键操作质量的重要因素。如何保证服务接口的正确性是面向服务计算中的关键问题。
事务是对物理和抽象的应用状态上的操作集合。如果事务执行过程中某个操作由于某些错误的发生而失败,就需要进行错误处理来进行失败恢复,使系统恢复到之前的状态。由于面向服务的系统处在一个开放的分布式环境中,其中某个事务中的操作涉及到的资源可能由不同的组织掌握和管理,在这种情况下,如果要求在事务执行过程中对所涉及的所有资源进行隔离是不现实的。基于服务的事务与传统事务的差别在于执行时间长,需要在运行时协商来提交事务,并且隔离的要求需要降低。因此,长事务模型更加适合于服务计算的要求。
具备长事务特征服务接口是服务接口中较为特殊的一类,它所代表的服务内部有长事务的特征。为了保证服务接口的正确性,形式化的服务接口验证方法是一种重要手段。当前的服务接口验证方法不能够支持对具备长事务特征服务接口的表示、性质规约和验证,如果使用一般的形式系统直接进行描述,比如状态机、进程描述语言或Petri网,则会过于复杂。此外,在系统语义层面的验证面临状态爆炸问题,从而使验证过程不能够终止。
因此,为了保证具备长事务特征服务接口的正确性,如何对具备长事务特征服务接口进行有效验证是一个重要的问题。
发明内容
本发明要解决的技术问题是:提出一种针对具备长事务特征服务接口的验证方法,可以基于接口模型,通过语法层面的搜索,来验证服务接口是否满足关键性质,以避免语义层面的验证所面临的状态爆炸问题。
解决本发明技术问题所采用的技术方案是:
第一步:使用自动机和函数来定义需要验证的具备长事务特征服务的接口。
在构建接口的过程中会使用到下面一些定义:
1.1接口动作是一个二元组,包括服务接口中的方法名m以及方法调用的一个结果o,表示名字为m的服务方法的一次调用,其结果为o。有两类动作,成功动作表示方法调用不会发生异常,异常动作表示方法调用会发生异常,在发生后需要进行失败恢复。
1.2具备长事务特征服务的接口包含四个部分:(1)给出接口动作调用关系的扩展协议自动机,其中包含可能出现的动作集A,自动机中的状态集合S(S中⊥是返回状态,
1.3协议项的形式有四种:如果形如a则表示需要引发动作a;如果形如
第二步:采用性质构造方法构造具备长事务特征服务接口需要满足的关键性质。
服务接口的关键性质用
第三步:根据关键性质的不同形式,使用相应的规则进行搜索来验证服务接口,最终得到服务接口是否满足关键性质。过程如下:
3.1初始化。置初始的结论集合为空集。
3.2搜索。根据不同的关键性质类型,使用不同的规则进行匹配,如果可以得到新的结论就把新的结论加到结论集合中,有下面几种情况:
3.2.1对形如
3.2.11如果状态是返回状态⊥或者异常状态
3.2.1.2如果状态s可以通过协议项a迁移到s′,则如果动作a不属于D,a的开始状态sa满足
3.2.1.3如果状态s可以通过协议项a·b迁移到s′,其中a·b可以是非确定选择协议项
3.2.2对于形如
3.2.2.1如果状态是返回状态⊥或者异常状态
3.2.2.2如果状态s可以通过协议项a迁移到s′,则如果动作a不属于D,a的开始状态sa满足
3.2.2.3如果状态s可以通过协议项a·b迁移到s′,其中a·b可以是非确定选择协议项
3.2.3对于形如
3.2.3.1如果状态s可以通过协议项a迁移到s′,并且动作a属于D2,则s满足
3.2.3.2如果状态s可以通过协议项
3.2.3.3如果状态s可以通过协议项
3.2.3.4如果状态s可以通过协议项a迁移到s′,则如果动作a不属于D1,并且a的开始状态sa满足
3.2.3.5如果状态s可以通过协议项
3.2.3.6如果状态s可以通过协议项
3.2.3.7如果状态s可以通过协议项a迁移到s′,则如果动作a不属于D1,a的开始状态sa满足
3.2.3.8如果状态s可以通过协议项a·b迁移到s′,其中a·b可以是非确定选择协议项
3.2.4对于形如
3.2.4.1如果状态s可以通过协议项a迁移到s′,并且动作a属于D2,则s满足
3.2.4.2如果状态s可以通过协议项
3.2.4.3如果状态s可以通过协议项
3.2.4.4如果状态s可以通过协议项a迁移到s′,则如果动作a不属于D1,并且a的开始状态sa满足
3.2.4.5如果状态s可以通过协议项
3.2.4.6如果状态s可以通过协议项
3.2.4.7如果状态s可以通过协议项a迁移到s′,则如果动作a不属于D1,a的开始状态sa满足
3.2.4.8如果状态s可以通过协议项a迁移到s′,则如果动作a不属于D1,a的开始状态sa满足
3.2.4.9如果状态s可以通过协议项
3.2.4.10如果状态s可以通过协议项
3.2.4.11如果状态s可以通过协议项
3.2.4.12如果状态s可以通过协议项
3.3判断在步骤3.2中是否增加了新的结论,如果有则转到步骤3.4,否则整个过程结束,服务接口不满足关键性质。
3.4判断。根据关键性质的不同类型,判断性质是否被满足。对于形如
采用本发明可以达到以下技术效果:
本发明是一种具备长事务特征服务的接口验证方法,可以作为对服务计算中具备事务特征服务的接口进行形式化验证的一种有效手段,与现有服务接口方法比较,本发明的优点在于接口验证方法能够涵盖服务中补偿和错误处理对应的接口行为,并且验证方法从接口的语法层面直接进行搜索,避免了从语义层面进行验证可能出现的状态爆炸问题。
附图说明
图1为验证方法的总体流程图。
图2为验证方法中第三步的流程图。
具体实施方式
本发明中公开了一种具备长事务特征服务接口的验证方法,方法的主要步骤见附图1。其中每一步解释如下:
1使用自动机和函数来定义需要验证的具备长事务特征服务的接口。
2采用性质构造方法构造具备长事务特征服务接口需要满足的关键性质。
3根据关键性质的不同形式,使用相应的规则进行搜索来验证服务接口,最终得到服务接口是否满足关键性质。
图2给出了上述验证方法中第3步接口验证的流程:
1初始化。置初始的结论集合为空集。
2使用规则进行搜索。根据不同的关键性质类型,使用不同的规则进行匹配,如果可以得到新的结论就把新的结论加到结论集合中,有下面几种情况:
2.1对形如
2.2对于形如
2.3对于形如
2.4对于形如
3判断是否得到了新的结论。在最近一次第2步中是否增加了新的结论,如果有则转到第4步,否则整个过程结束,服务接口不满足关键性质。
4根据关键性质的不同类型,判断性质是否被满足。对于形如
机译: 服务器,车辆,分布式事务验证系统和分布式事务验证方法
机译: 对象例如人,识别/验证方法,涉及提取特征特征,并将特征与存储在数据库中并在特定时间点检测到的对象的特征特征进行比较
机译: 双通信服务接口,用于分布式事务处理