Model Checking Inconsistency Recovery Costs

  • Gang Zhou
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7221)


Typically, when services become inconsistent from a business viewpoint, it is expected that compensation be used to recover from the inconsistency, by undoing the executed operations. In reality, compensation may incur additional costs, however existing approaches to recovery do not take such costs fully into account. We identify some major underlying gaps in SOC (Service Oriented Computing) related to compensation modelling, inconsistency identification, recovery and cost calculation. To make services more reasonable and predictable in dealing with inconsistencies from a cost perspective. We propose a cost-aware compensation framework modelling service compensations and compositions by a Petri Net-based model, reasoning about inconsistency recovery behaviours by model checking the LTL properties corresponding to business rules, and computing costs of recovery behaviours by parameterised cost calculation.


Model Check Composition Operator Service Composition Linear Temporal Logic Business Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Abdulla, P.A., Mayr, R.: Minimal Cost Reachability/Coverability in Priced Timed Petri Nets. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 348–363. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  2. 2.
    Acu, B., Reisig, W.: Compensation in Workflow Nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 65–83. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Alur, R., et al.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Andrews, T., et al.: Business process execution language for web services, version 1.1. Standards proposal by BEA Systems, International Business Machines Corporation, and Microsoft Corporation (2003)Google Scholar
  6. 6.
    Beyer, D., Chakrabarti, A., Henzinger, T.A.: Web service interfaces, pp. 148–159 (2005)Google Scholar
  7. 7.
    Billington, J., Christensen, S., van Hee, K.M., Kindler, E., Kummer, O., Petrucci, L., Post, R., Stehno, C., Weber, M.: The Petri Net Markup Language: Concepts, Technology, and Tools. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 483–505. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Biswas, D.: Compensation in the World of Web Services Composition. In: Cardoso, J., Sheth, A.P. (eds.) SWSWPC 2004. LNCS, vol. 3387, pp. 69–80. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Bonet, P., et al.: PIPE v2. 5: A Petri net tool for performance modelling. In: Proc. 23rd Latin American Conference on Informatics (CLEI 2007). Citeseer (2007)Google Scholar
  10. 10.
    Bunting, D., et al.: Web Services Composite Application Framework (WS-CAF). Ver1. 0 (2003)Google Scholar
  11. 11.
    Butler, M., Ferreira, C.: A process compensation language, pp. 61–76 (2000)Google Scholar
  12. 12.
    Butler, M., Hoare, T., Ferreira, C.: A Trace Semantics for Long-Running Transactions. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) CSP25. LNCS, vol. 3525, pp. 133–150. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Cabrera, F., Copeland, G., Cox, B., Freund, T., Klein, J., Storey, T., Thatte, S.: Web services transaction (WS-transaction). In: Microsoft, IBM etc (2002)Google Scholar
  14. 14.
    Choi, S., et al.: A framework for ensuring consistency of Web Services Transactions. Information and Software Technology 50(7-8), 684–696 (2008)CrossRefGoogle Scholar
  15. 15.
    Coleman, J.: Examining BPEL’s compensation construct. In: Rigorous Engineering of Fault-Tolerant Systems (REFT 2005), p. 122 (2005)Google Scholar
  16. 16.
    Fischer, J., Majumdar, R.: Ensuring consistency in long running transactions. In: Proceedings of the Twenty-Second IEEE/ACM International Conference on Automated Software Engineering, pp. 54–63. ACM (2007)Google Scholar
  17. 17.
    Garcia-Molina, H., Salem, K.: Sagas. ACM SIGMOD Record 16(3), 249–259 (1987)CrossRefGoogle Scholar
  18. 18.
    Gray, J.: The transaction concept: Virtues and limitations. In: Proceedings of the Very Large Database Conference, pp. 144–154. Citeseer (1981)Google Scholar
  19. 19.
    Greenfield, P., et al.: Compensation is not enough. In: Proceedings of the 7th International Conference on Enterprise Distributed Object Computing, p. 232. IEEE Computer Society, Washington, DC (2003)CrossRefGoogle Scholar
  20. 20.
    Holliday, M.A., et al.: A generalized timed Petri net model for performance analysis. IEEE Transactions on Software Engineering (12), 1297–1310 (1987)Google Scholar
  21. 21.
    Kramer, J., McGee, J.: Concurrency: State Models and Java Programs (1999)Google Scholar
  22. 22.
    Li, J., Zhu, H., Pu, G., He, J.: Looking into compensable transactions. In: 31st IEEE Software Engineering Workshop, SEW 2007, pp. 154–166. IEEE (2007)Google Scholar
  23. 23.
    Lin, L., Liu, F.: Compensation with dependency in web services compositions. In: International Conference on Next Generation Web Services Practices, NWeSP 2005, pp. 183–188. IEEE (2006)Google Scholar
  24. 24.
    Massuthe, P., Schmidt, K.: Operating guidelines-an automata-theoretic foundation for the service-oriented architecture. In: Fifth International Conference on Quality Software (QSIC 2005), pp. 452–457. IEEE (2005)Google Scholar
  25. 25.
    Papazoglou, M.P., Georgakopoulos, D.: Service-oriented computing. Communications of the ACM 46(10), 25–28 (2003)CrossRefGoogle Scholar
  26. 26.
    Pires, P.F., et al.: Webtransact: A framework for specifying and coordinating reliable web services compositions (2002)Google Scholar
  27. 27.
    Potts, M., et al.: Business Transaction Protocol Primer. OASIS Committee Supporting Document (2002)Google Scholar
  28. 28.
    Reisig, W.: Simple Composition of Nets. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 23–42. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  29. 29.
    Vardi, M.: An Automata-Theoretic Approach to Linear Temporal Logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Gang Zhou
    • 1
  1. 1.School of CSITRMIT UniversityMelbourneAustralia

Personalised recommendations