Invited Talk III

Recently, long running transactions attracted much research attention, because they are adopted in distributed systems, such as service-oriented systems, to ensure consistency. How to model and verify long running transactions is critical to improve the reliability of current distributed systems. This talk will introduce our recent work on formal modeling, verification and refinement of long running transactions in terms of a process algebra language. The start point of our work is Compensating CSP (cCSP), which extends CSP for specification and verification of long running transactions. We present an extended cCSP to support the modeling of non-determinism, deadlock and livelock, which are the three basic features of concurrent systems. A full semantic theory supporting refinement for the extended language is developed based on the theory of CSP. Leveraged by our semantic theory, the verification techniques and the tools, such as FDR and PAT, can be extended for verifying long running transactions. This talk is based on joint work with Zhenbang Chen and Zhiming Liu.