基于CSP的Web服务无状态定义和可伸缩性验证

理论计算机科学电子笔记151（2006）71-87www.elsevier.com/locate/entcs基于CSP李·蒙塔汉，安德鲁·马丁和A. W. 罗斯科1号牛津大学计算实验室，牛津OX1 3QD，英格兰摘要会话和无状态等术语在Web服务的分类中被广泛使用。 我们使用CSP进程代数给出这些术语的正式定义。 在这一框架内，我们 还定义了面向服务的体系结构的概念。然后，这些定义用于证明无状态服务的重要可伸缩性。形式主义的使用应该允许最近的辩论，关于网络服务如何以及是否提供标准化的访问状态，以更严格的进展。关键词：分布式系统，形式化方法，Web服务，通信顺序进程（CSP）1引言目前在Web服务和网格社区中存在一个关于Web服务是否以及如何允许访问状态的争论。一种观点是没有状态的概念辩论因缺乏形式和明确性而受到阻碍。本文通过定义在辩论中使用的一些关键术语，在通信顺序过程（CSP）[3]形式主义中做出贡献这项工作的动机主要不是Web服务的正式验证（尽管这可能是一个可能的结果），而是为了更深入地理解这些概念。我们希望更多的原则性比较1电子邮件：{leemo，apm，awr}@ comlab.ox.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.03772L. Momtahan等人理论计算机科学电子笔记151（2006）71根据这些定义，可以提出不同的建议，使进入国家的机会1.1概述在第2节中，我们引用了Web服务分类下一节给出了CSP中的一系列第4节讨论了这种形式化分类法的一些含义。第5节总结了主要结论。第一个附录以另一种形式给出了我们的定义，可以与CSP模型检查器FDR一起使用。第二个附录给出了文中所用定理的证明2状态和服务我们在本节中的意图是说服读者，使用自然语言来定义会话和无状态这两个术语是不合适的，并且在当前的文献中，这些定义的清晰度很差。在[1]中，给出了以下Web服务的分类• 无状态服务实现消息交换，不访问或使用输入消息中不包含的信息。一个简单的示例是压缩和解压缩文档的服务，其中文档在与服务的消息交换中提供• 会话服务实现一系列操作，使得一个操作的结果取决于先前的操作和/或为后续操作做准备。服务使用消息逻辑流中的每个消息来确定服务的处理行为给定操作的成功是基于逻辑序列中前面的消息的处理许多交互式Web站点通过使用HTTP会话和Cookie来实现此模式。• 作用于有状态资源的服务根据它发送和接收的消息提供对一组逻辑有状态资源（文档）的访问或[1] 继续说：当我们在第三个模型中谈论作用于有状态资源的服务时，我们指的是其实现针对动态状态执行的服务服务在与请求者进行消息交换时所负责的状态。作用于有状态资源的服务可以L. Momtahan等人理论计算机科学电子笔记151（2006）7173如果它将状态管理的责任委托给另一个组件（如数据库或文件系统），则被描述为无状态。定义中使用的措辞在[1]的v1.0和v1.1之间发生了重大修改，这可能表明在自然语言中定义这些概念的一个相关的定义是面向服务的体系结构（SOA）上下文中的服务[4]给出了以下结果：服务是一组定义良好的操作，它是自包含的，无状态的，并且不依赖于其他服务的状态。. .这里，无状态意味着每次消费者与Web服务交互时在服务调用的结果被返回之后，动作就完成了。不存在后续调用与先前调用相关联的假设。3CSP中的Web服务在本节中，给出了一系列定义，这些定义构建了我们的Web服务模型及其分类法。不熟悉CSP表示法的读者可以参考附录A获得简要介绍。定义3.1无状态J（P）惠率s：traces（P）·P=P/s我们第一次尝试定义进程P的无状态概念是说，在传递任何事件之后，进程返回到其初始状态。只有当典型的请求-响应2操作被建模为单个事件时，这个定义才是令人满意的但是我们要考虑服务器与后端有状态资源的交互，这通常发生在请求和响应消息之间，因此必须将请求和响应建模为单独的事件。3.1线程我们首先定义一个CSP进程W，它愿意接受通道响应和请求上的任何事件，只要事件在请求和响应之间交替，并从请求开始。2其他类型的操作，如请求-响应，在本文中没有建模，但是我们希望我们的工作可以很容易地扩展到处理这些其他类型。74L. Momtahan等人理论计算机科学电子笔记151（2006）71定义3.2W=请求？x→WJWJ=响应？y→W为了方便起见，我们还将αW定义为所有请求和响应事件。定义3.3我们现在定义一个线程。αW ={|请求，响应|}定义3.4Thread（P）惠P = P |[αW] |Winitials（P）{|请求|}因此，如果进程P是一个线程，它在请求和响应事件之间交替，并且在收到第一个请求之前什么也不能做除此之外，事件可能随时发生。3.2无状态线程我们对无状态线程的定义如下，其中last（s）返回跟踪s中的最后一个事件。定义3.5无状态（P）惠线程（P）痕量：痕量（P）|public int findDuplicate（s）{|响应|}·P/s = P因此，如果一个线程P在传递一个响应事件后总是返回到它的初始状态，那么它就是无状态的。3.3可扩展线程我们定义了线程可以展示的另一个属性，我们称之为可扩展性。定义3.6可扩展（P）惠线程（P）P =（P|||P）|[ αW] |WL. Momtahan等人理论计算机科学电子笔记151（2006）7175这就是说，在W存在的情况下，它具有将未完成请求的数量限制为一个的效果，P的两个副本的行为就像一个。在推论C.8中，我们证明，从这个定义可以得出P =（P|||P |||P）|[αW]|W. 实际上，当任意数量的P在W存在的情况下交织时，所得到的我们还在定理C.6中证明了Stateless（P）等于Scalable（P）。有趣的是，相反的情况并不成立。请考虑：P（n）=请求。上→响应。ok→P（n+1）Q（n> 0）&请求。下→响应。k→P（n−1）P（0）是可伸缩的，但不是无状态的。我们注意到，虽然P（0）=（P（0）|||P（0））|[αW] |P（0），对交错组合的请求必须被转发到正确的线程，即可以接受事件的一个，并且交织算子的这一特征如果P是无状态，请求可以被转发到任何一个线程，因为两者总是接受相同的事件。3.4示例下面定义了一个进程P，其中无状态（P）成立：P=请求？name→如果已清除（name），则（商店。名称→响应。ok→P）Q其他（完整答案。失败→P）反应失败→P这个过程模拟了一个非常简单的航空公司订票系统中使用的线程预订请求是以乘客的姓名提出的如果乘客通过了安检，则会尝试通过事件将他们添加到乘客列表（一个辅助店名称，否则将被拒绝。乘客仍然可以被拒绝，如果乘客是满的。76L. Momtahan等人理论计算机科学电子笔记151（2006）71下面定义一个进程P（0），Thread（P（0））对它成立，但是无状态（P（0））不：P（x）=请求？n→如果清除（名称），则（（x#s T {|响应|}引理C.4initialsQs {|响应|}= 0initialsRs {|请求|}= 0证据 这是Thread（P）的一个简单结果。Q约定C.5并行运算符（parallel operator）的接口是αW，除非另有说明。该交织算子（|||）比并行运算符绑定得更紧。例如 P |||PW代表（P|||P）|[ αW] |W定理C.6无状态（P）可扩展（P）证据假设无状态（P）。 我们表明，在我们的假设下，对于每一个痕迹，P||| P的所有迹t：（P |||P W）/t =（P/t）|||P/W = P/t如果t = last（t）∈ {|响应|}（P |||P W）/t =（P/t）|||P W ′= P/t否则因此（P |||P）W = P，即可扩展（P）。为了证明上述等式，我们证明了这些项的初始、拒绝和初始发散是相等的，并且如果我们假设上述陈述，则在每个初始事件之后，结果状态也是相等的。这可以通过参考CSP中的构造性递归和唯一固定点（UFP）理论来正式证明[5]。我们注意到，由于无状态（P），如果x ∈ {|响应|}则Qs-（x）= Q（x）.84L. Momtahan等人理论计算机科学电子笔记151（2006）71情形（i）P1 = Q（n）P2 = Q（n|||Q（Q）首字母（P1）=首字母（P2）拒绝（P1）=拒绝（P2）发散（P1）惠发散（P2）x：首字母（P1）·P1/x：首字母（P2）·P2/=（R（x）|||Q（W ′）Q（Q（|||R（xW ′）=R（x）|||Q（Q）情况（ii）P 1 = RsP 2 = Rs|||Q（W ′.首字母（P1）=首字母（P2）拒绝（P1）=拒绝（P2）发散（P1）惠发散（P2）x：初始值（P1）·P1/如果x ∈ {|响应|} then Qs-（x ∈ {\displaystyle{\displaystyle {x}}}）else Rs-（x ∈{\displaystyle {\displaystyle {x}}}）|响应|}则Q（X）else Rs-（X）x：首字母（P2）·P2/如果x ∈ {|响应|}则Qs-（x ≠ 0 |||Q（Q）else Rs-（x≠ 0|||Q（W ′）=如果x ∈ {|响应|}，则Q（|||Q（Q）else Rs-（x≠ 0|||Q（Q）Q定理C.7P|||P |||P W = P|||（P |||P W）W证据这个定理的证明是基于与前一个类似的技术。我们通过显示以下等式来覆盖所有可达状态Qs|||Qt|||QvW = Qs|||（Qt|||QvW）WRs|||Qt|||Qv<$W ′= Rs|||（Qt|||Qv W）L. Momtahan等人理论计算机科学电子笔记151（2006）7185W ′Qs|||Rt|||Qv<$W ′= Qs|||（Rt|||QvW ′）W ′Qs|||Qt|||RvW ′= Qs|||（Qt|||RvW ′）W ′也就是说，如果我们假设上述陈述，我们证明了这些项的初始，拒绝和初始分歧是相等的，并且结果状态也是相等的86L. Momtahan等人理论计算机科学电子笔记151（2006）71情况（i）P1 = Qs|||Qt|||QvWP 2 = Qs|||（Qt|||QvW）W。首字母P1 =首字母Qsn首字母Q t n首字母Q v =首字母P 2拒绝P 1 =拒绝Qs n拒绝Q t n拒绝Q v =拒绝P 2发散P1惠发散Q s n发散Qsn发散Qv惠发散P 2x：首字母P1·P 1/Hi：{s，t，v} |x ∈ initial（P/i）·如果x∈/{|request|然后（i = s）&（Qs-（x）|||Qt|||QvW）Q（i = t）&（Qs|||Qt-（x |||Qv W）Q（i = v）&（Qs|||Qt|||Qv-（x W）其他（i = s）&（Rs-（x）|||Qt|||QvW ′）Q（i = t）&（Qs|||Rt-（x |||QvW ′）Q（i = v）&（Qs|||Qt|||Rv-（x W ′）x：首字母P2·P 2/Hi：{s，t，v} |x ∈ initial（P/i）·如果x∈/{|request|然后（i = s）&（Qs-（x）|||（Qt|||QvW）W）Q（i = t）&（Qs|||（Qt-（x）|||QvW）W）Q（i = v）&（Qs|||（Qt|||Qv-（x W）W）其他（i = s）&（Rs-（x）|||（Qt|||QvW）W ′）Q（i = t）&（Qs|||（Rt-（x）|||QvW ′）W ′）Q（i = v）&（Qs|||（Qt|||Rv-（x <$W ′）<$W ′）L. Momtahan等人理论计算机科学电子笔记151（2006）7187情况（ii）P1 = Rs|||Qt|||Qv<$W ′<$P 2 = Rs|||（Qt|||Qv W）W ′.首字母P1 =（initials Rs initials Qtinitials Qv）− {|请求|联系我们首字母P2拒绝P1 ={r：refusals Rs|r − {|请求|} ∈ refusals Qt<$refusals Qv}=拒绝P2发散P1惠发散Rs发散Qt发散Qv惠偏离P2x：首字母P1·P 1/Hi：{s，t，v} |x ∈ initial（P/i）·如果x∈/{|res pons e|然后（i = s）&（Rs-（x）|||Qt|||QvW ′）Q（i = t）&（Rs|||Qt-（x |||QvW ′）Q（i = v）&（Rs|||Qt|||Qv-（x W ′）其他（Qs-（x）|||Qt|||Qv W）x：首字母P2·P 2/Hi：{s，t，v} |x ∈ initial（P/i）·如果x∈/{|res pons e|然后（i = s）&（Rs-（x）|||（Qt|||QvW）W ′）Q（i = t）&（Rs|||（Qt-（x）|||QvW）W ′）Q（i = v）&（Rs|||（Qt|||Qv-（x W）W ′）其他（Qs-（x）|||（Qt|||QvW）W）88L. Momtahan等人理论计算机科学电子笔记151（2006）71情形（iii）P1 = Qs|||Rt|||QvW ′P 2 = Qs|||（Rt|||QvW ′）W ′.首字母P1 =（initials Qsinitials Rtinitials Qv）− {|请求|联系我们首字母P2拒绝P1 ={r：refusals Rt|r − {|请求|} ∈ refusals Qs <$refusals Qv}=拒绝P2发散P1惠发散Rs发散Qt发散Qv惠偏离P2x：首字母P1·P 1/Hi：{s，t，v} |x ∈ initial（P/i）·如果x∈/{|res pons e|然后（i = s）&（Qs-（x）|||Rt|||QvW ′）Q（i = t）&（Qs|||Rt-（x |||QvW ′）Q（i = v）&（Qs|||Rt|||Qv-（x W ′）其他（Qs|||Qt-（x |||Qv W）x：首字母P2·P 2/Hi：{s，t，v} |x ∈ initial（P/i）·如果x∈/{|res pons e|然后（i = s）&（Qs-（x）|||（Rt|||QvW′）W ′）Q（i = t）&（Qs|||（Rt-（x）|||QvW ′）W ′）Q（i = v）&（Qs|||（Rt|||Qv-（x <$W ′）<$W ′）其他（Qs|||（Qt-（x）|||QvW）W）情形（iv）P1 = Qs|||Qt|||RvW ′P 2 = Qs|||（Qt|||RvW ′）W ′. 同样。Q推论C.8可扩展（P）P = P |||P |||P WL. Momtahan等人理论计算机科学电子笔记151（2006）7189证据可扩展（P）P = P |||P W = P|||（P |||P W）W P|||（P|||PW）W = P|||P|||PW可扩展（P）P = P |||P |||P WQ