2相关理论概述
形式化方法作为一种对Web服务进行建模并ii检测系统足朽满足一致性属性的重要方法，得到了很多的关注。要完成形式化方法的整个过程，第1步就需要对被测系统进行建模，也即使用形式化的规范语言将被测系统描述出来。其次对用户关心的一致性等属性进行建模，使用时序逻辑属性语言将属性描述出来，然后选择相应的形式化检测工具检测待测系统是否满足这些属性，最后得出结论，并得出正例‘或反例，以支持Web服务检测中下一阶段的工作，即使用TTCN-3对部署好的Web服务进行测试，对测试用例的选择能够产生一定的指导作用。本章将对形式化方法中涉及的实现Web服务流程的BPEL规范，形式化方法框架中的形式化规范语言LOTOS，属性描述语言以及模型检测技术做详细的介绍。
2.1 BPEL 规范
“BPEL ( Business Process Execution Language )即业务流程执行语言，是在以XML、Web服务为基础的诸多标准之上提出的一种新型的业务流程定义语言”它定义了中心流程与其他参与业务实现的服务之间的交行为，并且这些交互符合标准的接口规范，BPEL中心流程仅仅通过服务地址，就可以直接调用遵循标准接口规范的服务。通过定义这些交互，BPEL中心流程可以作为一个独立的服务对外提供服务，用以完成复杂的业务需求。要对Web服务组合进行形式化建模，首先必须了解实现商业过程组织的规范语言——BPEL。本章首先介绍BPEL经历的几个历史阶段，然后介绍BPEL中最关键的核心活动，其后将阐述BPEL的其他结构，最后说明BPEL的特点和相关技术。
2.1.1 BPEL发展简史
Web服务业务流程执行语言WS-BPEL的前身是Microsoft的XLANG和IBM的WSFL(Web Services Flow Language,网络服务流程语宫)，"XLANG是一种由专门的控制构件构成的结构化的流程建模语言，而WSFL足种基于加入（join)和转换（transition)条件的、图形化的建模语言.WSFL可以根据流程模式进行图形化的建模，具有很强的直观性，易于图形化建模工具的支持，这两种建模语言都有很大的用户群”。2002年8月，IBM、Microsoft和BEA为了规范业务流程模型，结合了 XLANG和WSFL两种语言的特点，联合发布了 BPEL4WS(BusinessProcess Execution Language for Web Services) , BPEL4WS 更方便人们进行具体的基于图形的建模，同时又可以将图形化建模的结果直接部署到可运行的环境上，使之可以提供服务。随后Siebel和SAP合作，将BPEL4WS1.0改良为BPEL4WSU版本，并在2003年5月发布，这个版本吸取了这两种规范的优点，既能够支持灵活直观的图形化表示，同时又增加了异常处理机制，使得标准更加完善。同时，OASIS 成立了 WS-BPEL 技术委员会(WS-BPEL TC)，2007 年 4 月 12 日，OASIS发布了 WS-BPEL2.0标准。BPEL规范发布后，由于其以Web服务为操作对象，并且基于XML技术和WSDL语言编写，与具体实现平台无关，具有幵放性、松稱合性、敏捷性和可重用性，得到了广泛的应用。
2相关理论概述.....................................8
2.1 BPEL 规范................................8
2.2系统建模语言................................14
2.3届性建模语言................................17
2.4模型检测技术................................18
3 BPEL流程的 LOTOS 建模................................20
3.1 LOTOS主行为框架的建立................................21
3.2基本活动的形式化建模................................22
3.3结构化活动的形式化建模................................26
3.4其他结构的形式化建模................................30
4模型检测规约方法的设计与................................32
4.1转换工其的设计................................32
4.2转换工其的实现...............................35
4.3规约方法的实现...............................36
6结 论
随着Web服务组合技术的FI益发展，对Web服务组合业务逻辑的建模与检验工作也将更加引起人们的重视。形式化方法作为一种具有数学背景的方法，其逻辑性也使验证的结果更加地令人信服，模型检测因其完备性而受到关注，但是它存在的状态空间爆炸问题又是研究人员使用该方法的所必须要解决的问题，CADP工具集中的模型检测器Evaluator采用状态缩减技术有效地解决了状态空间爆炸的问题。可见，形式化方法可以对BPEL规范进行有效的描述和检测。关于形式化建模与检测，工业界己经给出了很多形式化描述BPEL业务流程的定义，他们使用不同的建模方法，采用不同的形式化描述语言来描述Web服务模型，对于属性的建模的方法也不尽相同，但是使用LOTOS建模方面的研究还比较少，并且未给出详细的映射方法，另外错误处理器和事务处理器等的映射工作也未尽完善，而且很多方法只是针对比较早期的BPEL4WS规范，并不支持WS-BPEL2.0规范中的出现的if、forEach等活动的建模，系统属性方面，大多釆用线性时序逻辑LTL描述，在描述能力方面也比较欠缺。
本文在模型检测的基础上，提出了一个Web服务组合的LOTOS形式化模型，能够比较全面的描述BPEL的各种活动，并且将新出现的几个活动也进行了映射，采用的LOTOS规范，模型检测器Evaluator和属性描述方法mu-演算具有一定的优越性，能够完备地描述出Web服务组合的业务逻辑，并且将所有可能的路径全部列举出来，同时采用mu-演算对系统要满足的属性进行了建模，能够详尽地描述Web服务组合系统的属性，基本满足检测系统安全性的要求，更保证了检测结果的可信性，同时为了方便对现有的BPEL建模，给出了将BPEL直接转换为LOTOS的工具，最后通过对两个实例进行形式化建模，说明了形式化方法的整个流程，并且给出检测结果，说明了开发的工具的可用性和实用性，能够满足各种复杂业务流程的.
参考文献
[17]Wing J. M. A Specifier's Introduction to Formal Methods[J], IEEE computer, 1990,23(9):8-24
[18] ISO/IEC 8807-1989, Information process systems, open systems interconnection,LOTOS A formal description technique based on the temporal ordering ofobservational behavior[S].
[19] serge P Hoogendoom，Piet H L Bovy. Dynamic user-optional assignment incontinuous time and space, Transportation Research Part, 2007: 571-592
[20] Andreas Schadschneider，Wolfgang Knospe, Ludger Santen. Michaelschreckenberg，optimization of highway networks and traffic forecasting. Physica，2005:165-173.
[21]D. Kozen. "Results on the Propositional Mu-Calculus." Theoretical ComputerScience, v. 27, p. 333-354, 1983.
[22]E. A. Emerson and C-L. Lei. "Efficient Model Checking in Fragments of thePropositional Mu-Calculus.” Proceedings of the 1st LICS, p. 267-278, 1986.
