An Operational Semantics For Verifying Extended CCSP

Service-Oriented Computing(SOC) provides a new computing paradigm for distributed computing. Usually, a task in SOC is accomplished by a coordination of different services, and the coordination is often carried out by a third party. The classical ACID transaction model and two-phrase protocol are not realistic for this scenario, because the third party can not isolate the resources of service providers. Long-running transaction(LRT) models are used as an important approach for ensuring the consistency of the service coordinations in a distributed environment.In order to ensure the correctness of the LRTs in SOC, some formal languages have been proposed to specify and verify LRTs. Compensating CSP extends CSP with the ability of modeling LRTs, and the extended cCSP improves cCSP with synchronization, internal choice, recursion, hiding, renaming and so on. The extended cCSP can effectively model the LRTs in a distributed environment. Until now, the extended cCSP only has denotational semantics, and does not have a complete operational semantics. Furthermore, there is no tool that can support the modeling and verification of the extended cCSP. This dissertation investigates the operational semantics and the general model checking problem with respect to regular properties for extended cCSP. On the basis of the operational semantics, we developed a model checker prototype for the extended cCSP. The main contributions are as follows.Based on the operational semantics of cCSP, we propose an operational semantics for the extended cCSP. The incompleteness problem of the operational semantics of cCSP is solved. Then, we have proved the correspondence relation between the failure-divergence semantics and the operational semantics.This dissertation studies the complexity of the verification problem of model checking regular properties for the extended cCSP. By reducing the problem to the halting problem of a Minsky 2-counter machine, which is known to be undecidable, we have proved that the verification problem is undecidable in general. On the basis of PAT, we have built a model checker for the extended cCSP. The tool supports the modeling, simulation, and verification of the extended cCSP. The verification includes linear temporal logic(LTL) model checking and the checking for reachability, deadlock, livelock, refinement and so on.We use two typical LRTs to demonstrate the language and the tool. The experimental results indicate that the tool can analyze and verify many different kinds of properties and performs well on the consumption of time and memory.