02013598

a

02013598 Ferreira, Carla Butler, Michael Using B refinement to analyse compensating business processes. Bert, Didier (ed.) et al., ZB 2003: Formal specification and development in Z and B. Third international conference of B and Z users, Turku, Finland, June 4-6, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2651, 477-496 (2003). 2003 Berlin: Springer EN D.3 F.3.1

http://link.springer.de/link/service/series/0558/bibs/2651/26510477.htm

Summary: 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.