An Operational Semantics for Model Checking Long Running Transactions

Compensating CSP (cCSP) is an extension to CSP for modeling long running transactions (LRTs). In our work, we extended the original cCSP with the ability of modeling non-determinism, deadlock and livelock. Until now, there is only a failure-divergence semantics for the extended cCSP, and there is no model checking or animating tool for it. In this paper, we present an operational semantics for model checking the extended cCSP. We prove that the general problem of model checking the extended cCSP with respect to regular properties is undecidable. Using the operational semantics, we have implemented an animator and a prototype model checker for the extended cCSP based on the platform Process Analysis Toolkit (PAT). In addition, a case study is given to demonstrate the tool.