Modeling And Verifying Business Transactions For Web Services

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.