【作者】 袁敏；

【导师】 黄志球；

【作者基本信息】 南京航空航天大学 ， 计算机应用技术， 2012， 博士

【摘要】 面向服务的计算(Service-Oriented Computing, SOC)是一种以Web服务作为基本组件的分布式计算模式，它支持开放、动态和异构环境下分布式应用的系统集成。Web服务正从最初关注描述、发布和交互向支持健壮的业务协作新阶段发展。为了保证面向服务的应用获得正确、一致的执行结果，大多数工作流和B2B协作应用程序都需要支持复杂的、长时间运行的业务事务。面向服务的业务流程除了关注服务组合业务流程的功能特性外，应该整合考虑合成之上的事务特性。如何设计正确的Web服务组合业务流程，让它们协同工作并保持一致，即确保面向服务的业务事务(Business Transactions for Services, BTS)正确地执行是当前一个具有挑战性的重要问题。本文从操作系统进程管理的视角提出了面向服务的业务事务的概念视图,将现阶段的事务处理归结为在业务流程执行过程中对服务、活动及流程的分层管理。从建模语言到验证方法、从建模分析到验证实现，本文为面向服务的业务事务的正确性保障建立了一套系统的解决方案。主要研究成果如下：(1)提出了一种支持非功能性描述的移动进程代数MPi-演算。根据应用语义需求引入进程作用域的概念，扩展了Pi-演算进程移动性的含义。用链接相对进程作用域的移动来表示进程的移动，使得MPi-演算能够描述组件之间交互行为的非功能属性，具有兼顾系统功能性和非功能性描述的表达能力。提出了一种膜互模拟关系，使得在进程作用域内部具有不同行为的两个进程也可以被认为是等价的，并引入了膜等价概念，得出与强/弱互模拟等价类似的性质。(2)提出了一种等价自动机转换的模型验证方法。MPi-演算能够被解释成标号迁移系统(Labelled Transition System, LTS)，NuSMV是基于Kripke结构(Kripke Structure, KS)的符号模型检验器，LTS与KS都属于状态自动机(StateAutomata)。根据元模型LTS和KS之间的语义映射关系，给出了从MPi-演算模型到NuSMV的输入语言SMV的语法转换规则。基于元模型定义的语义映射关系和语法转换规则可以提高模型转换的可复用性和可移植性。(3)在服务层研究了如何保持业务流程参与者之间的协调一致性问题，提出了支持业务事务验证的服务协调模型。针对Web服务事务标准(WS-TX)定义的参与者之间交互消息缺乏严格的语义，用Pi-演算形式化描述了WS-TX规范中定义业务活动事务的WS-BA协议，在此基础上建立了适用于多个参与者的服务协调模型，并验证分析了协议的安全性和活性。实验结果表明，基于服务协调模型的业务事务验证方法，能够有效地提高业务流程执行的可靠性和一致性。(4)在活动层研究了如何利用Web服务事务模型分析事务的等价性问题，提出了面向服务的柔性事务建模与分析方法。用MPi-演算对柔性事务模型进行了形式化描述，考虑进程行为的事务依赖性，提出了一种事务膜等价关系。通过一个典型的柔性事务实例，阐述了利用事务膜开互模拟分析事务等价关系的方法。实验结果表明，事务膜开互模拟分析方法能够判别事务等价关系，约简目标系统模型，有效降低系统验证的复杂度。(5)在流程层研究了如何保证跨组织业务流程的可靠性问题，提出了跨组织多业务事务的建模与验证方法。将进程的动作交互与跨组织膜活动建立动态关联，提出了跨组织多业务事务建模方法。验证分析了多业务事务中排他性、响应性、非阻塞性和非平凡性等关键性质。实验结果表明，对于复杂的多业务事务，经过抽象或分解后，同样能够采用该方法保障多业务流程在设计与实现过程中的可靠性。(6)提出了基于策略的面向服务的业务事务验证支撑系统框架，提供了一种事务运行时的验证机制。设计和实现了面向服务的业务事务形式化验证原型工具VBT4S(Verification ofBusiness Transactions for Services)，支持主流开源的符号模型检验器NuSMV2。实验结果表明，系统支持非功能属性(如事务的完整性和一致性等)相关命题性质的模型检测，具有功能和非功能性质的统一验证与分析能力。更多还原

【Abstract】 Service Oriented Computing (SOC) is an emerging paradigm for distributed computing that usesservices as basic computational entities. SOC supports distributed application system integration inthe open-ended, dynamic and heterogeneous environment. Web services are moving from their initialcapability of description, publication and interaction to a new stage in which the robust businesscollaboration is supported. To ensure that service-based applications achieve correct and consistentoutcomes, most of the workflows and the B2B collaboration applications need to support complexand long-running business transactions. In addition to functional features of the business processprovided by service compositions, we should bring into consideration transactional features abovecompositions in business processes for services. How to verify correctness in the design of businessprocess provided by service compositions and keep them in consistent agreement on the outcomesfrom their working together, that is, correctness verification in the implementation of businesstransactions for services (BTS), is a challenging and important problem. A conceptual view of BTS isproposed in this paper from a process-management perspective in the operating system. Thetransaction processing at this stage is boiled down to the layer management of services, activities andprocesses during the execution of business processes. From modeling languages to verificationmethods, and then from modeling analysis to verifying implementations, a systemic solution isproposed to ensure the correctness of BTS. The main contributions of this dissertation are summarizedas follows:Firstly, a calculus of mobile processes named MPi-calculus is proposed in support of thenon-functional specifications. According to the requirements of application semantics, the concept ofthe process scope is introduced, and then the meaning of the process mobility is extended. Themovement of a process can be represented entirely by the movement of its links relative to its scope.This enables MPi-calculus to describe non-functional attributes of interactive behaviour between thecomponents and to have the expressive power for describing the functional and non-functionalcharacteristics. A new relationship named membrane bisimulation is proposed, which allows twoprocesses to be considered equivalent even if they have dissimilar patterns of the behaviour insidetheir process scope. The membrane equivalence is introduced, and then some properties similar to thestrong/weak equivalence are obtained.Secondly, a model verification methodology is proposed by equal value transformation of the finite state automaton. Traditionally the behavior of MPi-calculus is modeled on a Labeled TransitionSystem (LTS), and a symbolic model checker named NuSMV is based on the transition relation of aKripke structure. LTS and KS are very similar and they can be seen as generalizations of stateautomata. According to semantic mapping relations between two meta-models, i.e., LTS and KS,syntactic transformation rules are presented from MPi-calculus processes to the input language ofNuSMV. These semantic mapping relations and syntactic transformation rules defined by meta-modelcan improve the reusability and portability of the model transformation.Thirdly, at the service-level, a service coordination model is proposed in support of the businesstransactions verification by studying the problem of how to keep consistent agreement among theparticipants involved in the business process. For the definitions of the message exchanges that takeplace between the process and each one of its partners in WS-TX standard lack the precise semanticdescriptions, the Pi-calculus description of the WS-Business Activity protocol (WS-BA) is given,which specifies coordination types for long running loosely coupled business transactions. A servicecoordination model for multi-participants is proposed based on the formalization of the messaginginteractions semantics in WS-BA. Then this research verifies a system whether the protocol satisfiesthe principles of safety and liveness. Experimental results show that the business transactionverification based on service coordination model can effectively enhance the reliability andconsistency in business process execution.Fourthly, at the activity-level, the modeling and analysis method of flexible transactions forservices is proposed by studying the problem of how to analyze transactional equivalence relationsusing Web services transaction model. The formal description of the flexible transaction model inMPi-calculus is given. A transactional membrane equivalence relation is defined by introducingtransactional dependencies of the process behaviour. A running example presents the methodanalyzing transactional equivalence relation with the transactional membrane open bisimulation.Experimental results show that this method can judge the transactional equivalence relation, andreduce the target system model. This will effectively decrease the complexity of system verification.Fifthly, at the process-level, the modeling and verification method of cross-organizationalmulti-business transactions is proposed by studying the problem of how to ensure the reliability in thedesign and implementation of cross-organizational business processes. In the modeling approach,transaction semantics are introduced by the connection between the process interactions andcross-organizational membrane activities. The model checker is employed for checking whether or not the multi-business transactions satisfy the given key properties such as excludability,responsibility, non-blocking and non-triviality. Experimental results show that this method worksequally well for complex multi-business transactions by completing the abstraction or decomposition.Lastly, a supporting system framework for verification of business transactions for services(VBT4S) based on the policy enforcement is proposed, which provides a mechanism for runtimeverification of transactions. A prototype system named VBT4S is designed and implemented, whichsupports the major open source symbolic model checker (e.g. NuSMV2). Experimental results showthat the system can support the specification of non-functional properties (e.g. transactional integrityand consistency), and provide approaches to formally verify and analyze functional andnon-functional properties in a unified way.更多还原