Compensable Programs - Formal Methods and Hybrid Real-Time Systems - page 362

- a new model can be built by adding healthiness conditions:
1. the model of designs is characterised by the left zero law ⊥ ; P = ⊥ and

the unit laws skip ; P = P = P ; skip
2. the model of Req 1 -healthy designs is captured as a subset of designs
that meet the new left zero law halt ; P = halt
3. the model in dealing with compensation is seen as a submodel of the
Req 1 -healthy designs which satisfies the left zero law fail ; P = P .
- the model extension is ecnomical since the original algebraic laws remain
valid.

References

1. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus.
Information and Computation 148(1), 1-70 (1999)
2. Alonso, G., Kuno, H., Casati, F., et al.: Web Services: Concepts, Architectures and
Applications. Springer, Heidelberg (2003)
3. Bhargavan, K., et al.: A Semantics for Web Service Authentication. Theoretical
Computer Science. 340(1), 102-153 (2005)
4. Bruni, R., Montanari, H.C., Montannari, U.: Theoretical foundation for compensa-
tion in flow composition languages. In: Proc. POPL 2005, 32nd ACM SIGPLAN-
SIGACT symposium on principle of programming languages, pp. 209-220. ACM,
New York (2004)
5. Bruni, R., et al.: From Theory to Practice in Transactional Composition of Web
Services. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) Formal Techniques
for Computer Systems and Business Processes. LNCS, vol. 3670, pp. 272-286.
Springer, Heidelberg (2005)
6. Bulter, M.J., Ferreria, C.: A process compensation language. In: Grieskamp, W.,
Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 61-76. Springer,
Heidelberg (2000)
7. Bulter, M.J., Ferreria, C.: An Operational Semantics for StAC: a Lanuage for Mod-
elling Long-Running Business Transactions. In: De Nicola, R., Ferrari, G.L., Mered-
ith, G. (eds.) COORDINATION 2004. LNCS, vol. 2949, pp. 87-104. Springer, Hei-
delberg (2004)
8. Butler, M.J., Hoare, C.A.R., Ferreria, C.: A Trace Semantics for Long-Running
Transactions. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating
Sequential Processes. LNCS, vol. 3525, pp. 133-150. Springer, Heidelberg (2005)
9. Curbera, F., Goland, Y., Klein, J., et al.: Business Process Execution Language
for Web Service (2003), http://www.siebei.com/bpel
10. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs
(1976)
11. Gordon, A.D., et al.: Validating a Web Service Security Abstraction by Typing.
Formal Aspect of Computing 17(3), 277-318 (2005)
12. Jifeng, H., Huibiao, Z., Geguang, P.: A model for BPEL-like languages. Frontiers
of Computer Science in China 1(1), 9-20 (2007)
13. Hoare, C.A.R.: Communicating Sequential Language. Prentice Hall, Englewood
Cliffs (1985)
14. Hoare, C.A.R., Jifeng, H.: Unifying theories of programming. Prentice Hall, En-
glewood Cliffs (1998)