理论计算机科学电子笔记105（2004）147-158www.elsevier.com/locate/entcsWeb服务协议James E.作者：David E.作者：Leslie Lamport微软弗里德里希·H沃格特汉堡-哈堡理工大学摘要我们描述了使用形式化的方法来指定和检查Web服务协议。Web服务原子事务协议在TLA+中指定，并使用TLC模型检查器进行检查。一项适度的调查显示了导致方案非预期行为的疏忽;通过对方案的澄清和变更纠正了这些疏忽。保留字：规范、标准、tla、验证1介绍Web服务（WS）旨在克服异构分布式应用程序的集成问题[2]。大量使用SOAP [9]约定进行消息交换的协议正在开发中目前和未来的应用将取决于这些协议的正确性。与任何分布式系统一样，WS协议可能允许难以理解的模糊行为，并且调试它们将非常困难。由于对基于互联网的系统的依赖正在急剧增加，因此这些协议正确运行非常重要。我们的目标是将形式化方法应用到WS协议的标准化过程中。为了测试我们的方法，我们选择了一个重要的例子，即WS原子事务协议[3]。（其中两位作者参与了1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.02.022148J.E. Johnson等人理论计算机科学电子笔记105（2004）147设计协议）。我们的经验表明，编写和模型检查TLA+规范可以帮助消除协议中的错误和TLA+可用于帮助实现WS协议标准设计所需的可靠性。我们还相信，编写正式的规范可以帮助设计WS协议的过程。2示例：Web服务原子事务在分布式应用系统中，像数据库和/或缓存这样的资源由不同的进程访问。如果资源WS Atomic Transaction（WS-AT）是为此目的而设计的协议。事务协议由发起者进程开始，并由事务协调器控制。 管理事务的资源注册表的参与者进程。在某些时候，发起者可以决定中止或尝试提交事务。粗略地说，协议的目标是保证发起者和参与者就事务是提交还是中止达成一致。协议的所有消息都发往或来自事务协调器。发起者和参与者之间的任何通信都是特定于应用程序的，不是协议的一部分WS-AT基于著名的两阶段提交（2 PC）协议[1]。但是，它有两个非标准特性。首先是注册流程。在教科书对2PC的描述中，注册经常被忽略。第二个非标准特性是，它根据期望管理的资源类型区分两类参与者，称为volatile和durable。缓存是易失性资源的一个例子;传统数据库是持久性资源。标准的2PC协议使用两个阶段，准备和提交。WS-AT使用三个阶段：为易变参与者做准备、为持久参与者做准备和提交。参加者可以在准备阶段开始前的任何时间注册。因此，持久参与者仍然可以在易变参与者的准备阶段注册3正式规范和TLA+WS协议标准应该精确地描述与互操作性相关的行为。它应该省略内部实现细节，比如记录何时写入稳定存储。它应该允许某人实现协议中的一方，而不需要知道协议中的J.E. Johnson等人理论计算机科学电子笔记105（2004）147149其他缔约方正在执行。因此，标准应该是对协议参与者允许的行为的统一和完整的描述。WS标准有正式的机制来指定XML数据结构的格式[10]和服务接口[5]。然而，它们通常没有精确指定协议的完整行为的方法。相反，他们采用的是对协议的非正式描述，这些描述可能是不精确的、模糊的或不完整的;他们经常没有考虑到不寻常的情况。标准对精确性和完整性的需求自然意味着 使用正式的方法。这种方法使用定义良好的语言，具有精确的语义，用于编写协议允许行为的正式规范。可以应用工具来分析这些行为，并帮助检查协议的正确性目前还没有一种被普遍接受的正式指定WS协议的方法。在某些规范中给出的状态表是朝着这个方向迈出的一步，但它们通常不像正式规范那样精确地编写。TLA+ [8]是一种用于编写并发系统高级规范的语言。与大多数特定语言不同，它基于数学而不是编程语言结构。这使得它非常有表现力。它没有像发送消息这样的操作的内置结构，但是语言的表达能力足够强，这样的操作很容易在规范中定义。因此，不必使用语言中内置的某些特定消息传递语义（例如，无损FIFO传递），而是可以指定想要对消息传递做出的任何假设WS-AT协议非常简单，用任何严肃的语言来描述。然而，正如下面第4节所解释的，在规范中有一个地方，一个进程的这可能很难在一些专门为分布式系统设计的语言TLA+已经被用来描述广泛的并发系统，因此我们相信它能够指定任何想要的WS协议。因为它是如此的数学化，TLA+对大多数工程师来说似乎是陌生的。然而，我们发现工程师可以很快学会阅读TLA+规范。学习编写TLA+规范似乎和学习一门新的编程语言一样难。150J.E. Johnson等人理论计算机科学电子笔记105（2004）147224在TLA+中对蛋白质进行建模在2003年夏天，我们开始了一个小项目来编写WS原子事务协议的TLA+其中两名作者是使用形式化方法的经验丰富的研究人员;另外两名作者是该特定协议的专家，参与了其设计。该项目历时21个月。这是一个后台活动，所以实际花费的时间并不多，也许11个人月。该项目的结果是由研究人员编写的TLA+规范，以及由设计师在研究人员的协助设计者已经阅读了协议规范，以确定它符合他们对协议功能的想法。它已经被TLC模型检查器检查过，以确定它是完整的（指定在接收到任何可能的消息时应该发生什么），并且它满足协议的基本正确性属性（对交易结果的研究人员最初得到了官方规格的初步版本[3]。(Its状态表是他们发现最有用的部分。）他们与设计师会面了三次，并通过电子邮件向设计师提问。我们面临的第一个任务是决定写什么样的规范。没有一个系统的“正确”的具体化的概念。具体化是一种抽象，旨在服务于某种目的。我们发现基本上有两种方法来建模协议。一个是忠实地将协议的描述形式化。第二个是编写一个更简单的模型，其主要目标是验证协议的完整性和正确性。我们选择了第二个选项。因此，我们在TLA +规范中，将多个状态从官方规范的状态表中这减少了协议状态的总数，使规范更容易检查。我们面临的其他建模问题是：• 发起方和协调方之间的通信是应该在内部进行还是通过消息进行。设计师们决定让它在内部进行。• 应该对消息传递基础设施做什么样的假设。设计者们决定这个规范应该允许消息被重新排序、丢失和复制。由于议定书的某些方面在官方说明中没有足够清楚地说明，J.E. Johnson等人理论计算机科学电子笔记105（2004）1471514规格。这方面的一个重要例子是登记程序。研究人员不明白为什么在协调器忘记了所有事务之后，来自新参与者的Register消息无法到达。这不能通过检查官方规范来解决，因为注册是在不同的标准中描述的（WS-Coordination协议标准[4]）。官方规范没有明确解释这两种方案之间的相互作用。我们最终决定让TLA+规范描述注册进程和协调器之间的必要同步，而不说明它是如何实现的。因此，规范具有一个进程的动作，该动作由另一个进程的状态上的谓词启用，而不描述第一个进程如何学习第二个进程的状态。(This在TLA+中很容易表达，但在基于通信自动机的特定语言中会很难。大多数任务包括解决这些问题，其中许多问题是在编写规范时才发现的。完整的规范由大约350行TLA+加上500行注释组成。一旦人们理解了协议的作用以及应该如何建模，实际上编写它的规范并不难。该规范非常适合模型检查。 TLC检查了包含四个粒子的模型是否满足基本一致性。对于这个模型，协议有大约500，000个可达状态，其最长的非重复行为包含45个状态。TLC在一台2处理器、2.4GHz的PC上花了大约41分钟检查了它。该协议足够简单，因此，考虑到通信模式的拓扑结构和事务参与者的不可分割性，该规范极不可能包含任何仅在更大的模型上才会出现的错误。我们的电子邮件没有发现核心持久2PC协议的任何重大问题。这是意料之中的，因为议定书的这一部分已经很好理解。然而，它确实暴露了注册和易失性2PC协议的几个问题。使用WS-Coordination协议来控制事务提交协议中的注册是新的，使用独立的易失性和持久性2 PC协议也是新的。这些新功能的相互作用比预期的要复杂得多。模型检查揭示了设计者没有预料到的协议行为。这导致了对官方规范的澄清和变更5TLA+协议规范概述带注释的完整TLA+规范太长，无法在此呈现;与大多数正式规范一样，很难理解-152J.E. Johnson等人理论计算机科学电子笔记105（2004）147out评论相反，我们描述了它的完整的规范发布在Web上 [7]。回想一下，该协议涉及一个发起者、一个事务协调器（transactioncoordinator，TC）和一组参与者。TC与参与者交换消息。如上所述，我们将启动器和TC建模为单个进程。该规范声明了常量参数Participant，它表示参与者的集合。我们只指定协议的安全属性（允许发生什么），而不是它的活性属性（最终必须发生什么）。这使得消息传递的表示非常简单。变量msgs表示曾经发送的所有消息的集合。 在实现中，将通过接收某些消息来启用的动作在规范中通过msg中的那些消息的存在来启用。回想一下，我们决定允许消息丢失、复制或无序接收。由于msgs是一个集合，所以消息可以以任何顺序接收。消息的丢失表示为即使启用了该操作，也不执行该操作。 （因为我们只指定了安全属性，所以不需要执行启用的操作。重复的消息传递是允许的，因为消息永远不会从msg中删除，所以一旦消息在集中，接收该消息的操作总是启用的。还有三个其他变量：iState是描述发起者状态的记录参与者p.协议的正确性用状态谓词一致性的不变性来表示。它断言协议没有处于不一致的final或finishing状态，也就是说，一个进程认为协议已提交，而另一个进程认为它已中止。它有两个独立的合取词，一个断言如果发起者已经达到提交状态则什么为真，另一个断言如果参与者已经达到提交状态则什么为真。这两个合取词在逻辑上并不独立，但我们并没有消除冗余，以便清楚地表明所断言的内容。 定义 如下所示。我们并不指望读者能详细地理解这个谓词，而是希望读者能理解这个具体化的本质上的数学性质。 TLA+使用的约定是，表示它们的合取或析取，缩进用于去掉括号。∆稠度=（iState=数据库。st=J.E. Johnson等人理论计算机科学电子笔记105（2004）147153数据库。res=参与者：[p]. st=[p]. st=[p]. res∈{“？”，请参阅tcData。st=参与者：[p]. st∈ {[p]. st=[p]. res∈{“？”，参与者：[p]. st=[p]. res=⇒ ∧iState=数据库。st=数据库。res=iState=数据库。st=参与者：[pp]. st∈ {[pp]. st=[pp]. res∈ {“？”，一个TLA+安全规范的形式为InitQ[Next]vars，其中Init是描述初始状态的谓词，Next是描述下一状态关系的公式，vars是规范变量的元组。 规范的大部分内容由Next的定义组成。它的高级定义是∆下 =TC内部参数TCRcvMsg参数P内部参数PRcvMsg其中四个析取项具有以下含义：• TCInternal描述了发起者和TC的• TCRcvMsg描述TC对接收到参与者消息的响应。• PInternal描述了参与者• PRcvMsg描述了参与者发起方不发送或接收显式消息。动作TCInternal被定义为A（未改变的pData），其中A是描述由154J.E. Johnson等人理论计算机科学电子笔记105（2004）147TC或启动器。这是其中一个分离。(An action将状态更改描述为变量的新值和旧值之间的关系，其中变量的引发出现表示新值，未引发出现表示旧值。∨数据库。st=参与者：tcData。reg[p]“挥发性”[tcDataEXCEPT！. st=msgsJ=msgsdest：{p∈Participant：tcData。reg[p] =保持不变的iState动作TCRcvMsg的形式为：m∈msgs：B，其中B是一个析取，每个析取表示接收到不同类型的消息m。我们以一种相当不寻常的方式写出了这些析取式。一个典型的子操作具有以下形式（B1P1）... （Bn其中，Bi（称为如果没有一个守卫为真，那么子动作等于假，没有步骤是可能的。为了能够检查我们的规范的完整性，我们希望TLC在评估这个子操作并发现没有一个守卫为真时标记一个错误。因此，我们将子操作写成情况B1→P1Q. QBn→Pn如果恰好有一个守卫为真，则这两个表达式具有相同的含义。但是如果没有一个守卫为真，则后一个表达式是unfined，导致TLC报告错误。 这是定义中的一个析取项 的TCR cvMsg。∨m是一个已提交的消息。好吧type=电子邮件tcData。st=→tcDataJ=[tcDataEXCEPT！. reg[m. src]=正常情况下，TC处于提交状态。在本例中，它设置tcData的元素。reg对应于要提交的发送方。TC结束挥发性准备并开始持久性准备。当它从每个注册为volatile的参与者接收到Prepared或ReadOnly消息时，它会执行此操作，并向每个注册为durable的参与者发送Prepare消息J.E. Johnson等人理论计算机科学电子笔记105（2004）147155∆初始化和终止时间已被取消，并且不发送任何消息。Q数据库。st=数据库。res=→未更改tcData未更改的消息iState、pData、msgsPInternal和PRcvMsg的定义是相似的，除了它们涉及对参与者集合的额外存在量化规范以Spec的定义结束，完整的规范，以及断言一致性和TypeOK不变性的定理，TypeOK是描述变量类型的状态谓词。(TLA+是一种无类型语言。）Spec =初始化REQ[下一个]变量定理Spec<$Q（TypeOK<$Consistency）这是TLC检查的定理。6更多抽象规格我们还编写了两个更高级别的规范--一个70行的抽象规范，它只描述发起者和参与者的行为;另一个中间级别的共享内存规范，它也描述事务协调器，但删除了所有消息。我们已经检查过，这两个更高级别的规范都是通过上述协议规范实现Web服务的目的是提供一个可互操作的标准框架，允许开发安全可靠的事务系统和应用程序。因此，我们不仅要指定WS-AT，还要指定构建在其上的系统。我们的抽象规范对此很有用，因为它比完整的规范更简单。完整的WS-AT协议规范可以在现代处理器上快速验证。但是，一旦完成了这一步，就不需要在每次验证客户端系统时都重新执行。TLC需要253秒来检查具有四个参与者的系统的完整规范的所有行为。但它可以在不到7秒的时间内检查4个参与者的抽象规范的行为。这种时间上的节省，伴随着状态空间大小的大幅减少，将允许检查客户端系统，如果TC忘记了事务，则事务已经提交，并且忽略m156J.E. Johnson等人理论计算机科学电子笔记105（2004）147更大的模型。通过提供客户端系统的抽象规范，可以进一步执行该过程，以便更有效地对客户端进行建模和验证。抽象的规范也可以用作其他协议的规范。例如，可以通过用使用不同通信拓扑的提交协议替换2PC来获得新协议。如果新协议满足抽象规范，那么客户端可以安全地使用它来代替WS-AT。在指定完全抽象的协议之前，我们使用共享内存指定了它的行为共享内存规范的长度与完整的协议规范相同。它指定了WS-AT协议的要求，这些要求与发送的消息无关。所有内部数据结构和基本转换都从完整的协议规范中保留下来。在WS-AtomicTransaction的设计过程中，对协议消息的细节进行了大量讨论。共享内存的规范，结合详细的设计，将有助于澄清问题。它将提供一个快速测试，以确定对规范的拟议更改是否影响语义，或者它是否只是表达相同基本协议的不同方式。更高级别的规范也可以用于解释和实验。任何设计活动的两个部分是确定构建什么和如何构建它。这两个部分形成了设计的两个层次-即需求和详细设计。每个级别通过迭代设计活动通知其他级别TLA+提供了一种通用语言，可用于精确指定这两个级别TLC模型检查器可以自动验证详细设计是否满足要求。这允许快速检查设计中的更改对要求的影响。模型检查还可以显示更改需求如何影响当前的详细设计。2 PC协议已经建立得很好，也很容易理解，所以对于WS-AT，我们从一开始就很清楚我们在构建什么。对于其他新系统，情况往往并非如此。需求随着详细设计而发展。一旦用户清楚地了解了一个系统实际上是做什么的，他们就会想到新的应用程序--许多都有新的需求。任何增加反馈的数量、频率或速度的工具都会加速设计过程。J.E. Johnson等人理论计算机科学电子笔记105（2004）1471577结论WS-AT规范包含了大量TLA+规范中没有的细节。它非常仔细地描述了数据格式和一些消息传递接口。这些是TLA+规范忽略的协议细节，TLA+规范仅描述其行为特性。这些细节都是直截了当的，相当没有争议。因此，TLA+规范描述了协议中在当前规范中通常不精确的部分，并忽略了协议中已经非常精确地指定的因此，TLA+补充了大多数现有标准中采用的方法。拥有TLA+规范可以帮助防止不同实现之间的不兼容性。对拟议标准的精确描述也有助于避免标准编写者之间的误解。在标准委员会中，讨论可能变得非常抽象。不同的人很容易以不同的方式解释陈述。数学公式是明确的。编写正式规范可以帮助设计协议。 能够 快速检查协议规范是否满足更抽象的规范可以加快设计过程。协议需求的高级规范也可以用于检查协议客户端的正确性。TLA+是编写标准的一种特别好的语言，因为它是基于普通数学的。这使得它的语义特别简单，因为根据定义，一个规范语言的语义是用该语言编写的规范到数学的翻译。 正如一位工程师对TLA+所说的那样，在数学书上。我们现在正在TLA+中指定其他WS协议。确认Colin Campbell在将我们的规范翻译成AsmL规范语言时发现了一个小错误。引用[1] 伯恩斯坦，宾夕法尼亚州，V. Hadzilacos和N. Goodman，[2] 盒子， D、理解GXA， 技术 报告， 微软公司（2002年），网址http://msdn.microsoft.com/library/en-us/dngxa/html/understan dgxa.asp。[3] 卡布雷拉湾例如，规范：Web Services Atomic Transaction（WS-AtomicTransaction）（ 2002 ） ， IBM Systems ， International Business Machines Corporation ， MicrosoftCorporation，Inc.网址http://msdn.microsoft.com/ws/2003/09/wsat/。158J.E. Johnson等人理论计算机科学电子笔记105（2004）147[4] 卡布雷拉湖F.例如，WebServicesCoordination（WS-Coordination）（2003），IBM Systems，International Business Machines Corporation，Microsoft Corporation。网址http://msdn.microsoft.com/ws/2003/09/wscoor/。[5] Christensen，E.，F.库尔贝拉湾Meredith和S. Weerawarana，Web服务描述语言（WSDL）1.1（2001），W3C Note，URLhttp://www.w3.org/TR/2001/NOTE-wsdl-20010315网站。[6] Gray，J. and A.事务处理：概念和技术，摩根考夫曼出版公司，旧金山，1993年。[7] 约翰逊，J。E、D. E. 朗沃西湖Lamport和F.H. Vogt，Specification of the Web ServicesAtomic Transaction Protocol，URL http://research.microsoft.com/users/lamport/tla/ws-at.html.它可以也被通过在Web上搜索去掉“wsatom-ictransac-tion-tlaspec“中的破折号后得到的26个字母的字符串找到。[8] 兰波特湖， “Specifying Systems,” Addison-Wesley, Boston,[9] Mitra，N.，Soap版本1.2第0部分：入门，技术报告，万维网联盟（W3C）（2003），URLhttp://www.w3.org/TR/2003/REC-soap12-part0-20030624/。[10] 汤普森，H。美国， D. Beech，M. Maloney和N. Mendelsohn，Xml模式，第1部分：结构（2001），W3C推荐，URLhttp://www.w3.org/TR/2001/REC-xmlschema-1-20010502/网站。
我的内容管理
展开
