Using B Refinement to Analyse Compensating Business Processes

摘要

This paper explores the refinement of compensating business processes, which are modelled in a heterogeneous notation that combines StAC and B. In our refinement approach, the StAC behavioural and compensation information are explicitly embedded in a B machine. As the resulting machine is standard B one can use the B notion of refinement to prove the refinement of business processes. We also show how the Atelier-B prover can help in constructing the gluing invariant.