Output details

Failure-divergence semantics and refinement of long running transactions

<10> This work establishes a failure-divergence theory that integrates as sub-theories the operational semantics, trace semantics, failures semantics, thus forming a sound and complete foundation for development of systems, e.g. web-services, with Long Running Transactions. It extends Compensating Communicating Sequential Processes (cCSP) with internal-choice, synchronization and recursion, and develops a fixed-point theory of failure-divergences. The significance is that the partial order also characterizes the notion of refinement, a known challenge for a process language with internal-choice and synchronization. The work is referenced by researchers in China, Macau, and Germany. In particular, a model-checker is being developed in China.