Towards the Formal Model and Verification of Web Service Choreography Description Language
The Web Services Choreography Description Language (WS-CDL) is a W3C specification for the description of peer-to-peer collaborations of participants from a global viewpoint. For the rigorous development and tools support for the language, the formal semantics of WS-CDL is worth investigating. This paper proposes a small language CDL as a formal model of the simplified WSCDL, which includes important concepts related to participant roles and collaborations among them in a choreography. The formal operational semantics of CDL is given. Based on the formal model, we discuss further: 1) project a given choreography to orchestration views, which provides a basis for the implementation of the choreography by code generation; 2) translate WS-CDL to the input language of the model-checker SPIN, which allows us to automatically verify the correctness of a given choreography. An automatic translator has been implemented.

title: Model Checking Dynamic UML Consistency
abstract: UML is widely accepted and extensively used in software modeling. However, using different diagrams to model different aspects of a system brings the risk of inconsistency among diagrams. In this paper, we investigate an approach to check the consistency between the sequence diagrams and statechart diagrams using the SPIN model checker. To deal with the hierarchy structure of statechart diagrams, we propose a formalism called Split Automata, a variant of automata, which is helpful to bridge the statechart diagrams to SPIN efficiently. Compared with the existing work on model checking UML which do not have formal verification for their translation from UML to the model checker, we formally define the semantics and prove that the automatically translated model (i.e. Split Automata) does simulate the UML model. In this way, we can guarantee that the translated model does represent the original model.

title: Towards the theoretical foundation of choreography
abstract: With the growth of interest on the web services, people pay increasinglyattention to the choreography, that is, to describe collaborations ofparticipants in accomplishing a common business goal from a globalviewpoint. In this paper, based on a simple choreography language and arole-oriented process language, we study some fundamental issues relatedto choreography, especially those related to implementation, includingsemantics, projection and natural projection, dominant role in choices anditerations, etc. We propose the concept of dominant role and somenovel languages structures related to it. The study reveals some cluesabout the language, the semantics, the specification and theimplementation of choreography.

title: Type Checking Choreography Description Language
abstract: The Web Services Choreography Description Language (WS-CDL) is a W3C specification developed for the description of peer-to-peer collaborations of participants from a global viewpoint. Currently WS-CDL has no rigorous static type checking. We believe that introducing a type system will exclude many design and description errors, and ensure desirable properties of the choreography specifications. In this paper, we took a core language CDL, which covers most of the important features of the WS-CDL, and is more convenient for the study. We developed the abstract syntax and operational semantics of CDL, and defined a collection of rules which can be used to check if choreography is well-typed. Moreover, we also proved some type safety theorems for CDL in the sense that well-typed choreography cannot get stuck. We show how the use of type information can allow us to gain confidence in the correctness of choreography.

title: Towards the Semantics and Verification of BPEL4WS
abstract: In this paper, we discuss the semantics of BPEL4WS language which is a de facto standard for specifying and execution workflow specification for web service composition and orchestration. We propose a language @m-BPEL that includes most primitive and structured activities of BPEL4WS, and define its semantics. As the Timed Automata (TA) is powerful in designing real-time models with multiple clocks and has well developed automatic tool support, we define a map from @m-BPEL into composable TA. Therefore, the properties we want to check can be verified in TA network correspondingly. Furthermore, we prove that the mapping from @m-BPEL to TA is a simulation, which means that the TA network simulates correctly the corresponding @m-BPEL specification. The case study with model checker Uppaal shows that our method is effective, and a Java supporting tool based on Uppaal model checker engine has been developed.

title: Semantics of BPEL4WS-Like Fault and Compensation Handling
abstract: BPEL4WS is one of the most important business process modelling languages. One distinct feature of it is the fully programmable fault and compensation handling mechanism, which allows the user to specify the compensation behaviors of processes in application-specific manners. In this paper, we present a formal operational semantics to a simplified version of BPEL4WS, with some important concepts related to fault and compensation handling proposed and discussed, especially, the compensation closure and the compensation context. We also discuss some insights into the BPEL4WS language and its implementation obtained from this study.

title: On Odd and Even Cycles in Normal Logic Programs
abstract: An odd cycle of a logic program is a simple cycle that has an odd number of negative edges in the dependency graph of the program. Similarly, an even cycle is one that has an even number of negative edges. For a normal logic program that has no odd cycles, while it is known that such a program always has a stable model, and such a stable model can be computed in polynomial time, we show in this paper that checking whether an atom is in a stable model is NP-complete, and checking whether an atom is in all stable models is co-NP complete, both are the same as in the general case for normal logic programs. Furthermore, we show that if a normal logic program has exactly one odd cycle, then checking whether it has a stable model is NP-complete, again the same as in the general case. For normal logic programs with a fixed number of even cycles, we show that there is a polynomial time algorithm for computing all stable models. Furthermore, this polynomial time algorithm can be improved significantly if the number of odd cycles is also fixed.

title: Complexity of argument-based default reasoning with specificity
abstract: In this paper we investigate the complexity of Dung and Son's approach to default reasoning with specificity. We show that the three decision problems: existence of extensions, brave reasoning and cautious reasoning are generally complete for the second level of the polynomial hierarchy. For some restricted cases, e.g., Horn and 2CNF default theories, all the three problems are intractable although classical brave reasoning in these cases is tractable. Finally, we show that stratification can not reduce the complexity of brave and cautious reasoning although it guarantees the existence of extensions.

title: Fixed-parameter tractability of disjunction-free default reasoning
abstract: In this paper, the parameter which is the source of the complexity of disjunction-free default reasoning is determined. It is shown that when the value of this parameter is fixed, the disjunction-free default reasoning can be solved in time bounded by a polynomial whose degree does not depend on the parameter. Consequently, disjunction-free default reasoning is fixed parameter tractable.

title: A Multi-Agent System for E-Business Processes Monitoring in a Web-Based Environment
abstract: In this paper, we present a multi-agent system MAGS for the e-business processes monitoring in a web-based environment. We classify the types of agents in MAGS by their monitoring capabilities. An algorithm is given to explain the mechanism of supervising and controlling the execution of business processes. An abstract model of alerts, which can give warnings of infringement on business policies, is proposed. Access control can also be realized by MAGS, which manifests in delivering different view of the business process to different roles participate in it. Being successfully adopted in a customer service management system, MAGS has been proven flexible and practical.

title: Complexity Results for 2CNF Default Theories
abstract: This paper is concerned with the complexity of default reasoning with 2CNF default theories (D,W) in which W is a set of literals and D is a set of 2CNF defaults. It is proved that the problem whether a literal occurs in at least one extension can be solved in polynomial time. But the problem whether a literal appears in all extensions is proved to be co-NP-complete. The complexity of some subclasses of 2CNF default theories is also analyzed.