Ensuring Well-Formed Conversations between Control and Operational Behaviors of Web Services

  • Scott Bourne
  • Claudia Szabo
  • Quan Z. Sheng
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7636)


Despite a decade’s active research and development, Web services still remain undependable. Designing effective approaches for highly dependable Web service provisioning has therefore become of paramount importance. Our previous work proposes a novel model that separates the service behavior into operational and control behaviors for flexible design, development, and verification of complex Web services. In this paper, we further this research with a set of conversation rules to facilitate the verification of rich conversations between control and operational behaviors. The rules are specified as temporal logic formulas to formally check rich conversation patterns. The proposed approach is realized using state-of-the-art technologies and experiments show its feasibility and benefits.


Model Check Control Behavior Operational Behavior Linear Temporal Logic Message Type 
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.
    Yu, Q., Liu, X., Bouguettaya, A., Medjahed, B.: Deploying and Managing Web Services: Issues, Solutions, and Directions. The VLDB Journal 17(3), 537–572 (2008)CrossRefGoogle Scholar
  2. 2.
    Vieria, M., Laranjeiro, N., Madeira, H.: Benchmarking the Robustness of Web Services. In: Proceedings of the 13th International Symposium on Pacific Rim Dependable Computing (2007)Google Scholar
  3. 3.
    Sheng, Q., Maamar, Z., Yahyaoui, H., Bentahar, J., Boukadi, K.: Separating Operational and Control Behaviors: A New Approach to Web Services Modeling. IEEE Internet Computing 14(3), 68–76 (2010)CrossRefGoogle Scholar
  4. 4.
    Benatallah, B., Casati, F., Toumani, F.: Web Service Conversation Modeling: A Cornerstone for E-Business Automation. IEEE Internet Computing 8(1) (2004)Google Scholar
  5. 5.
    Bhiri, S., Perrin, O., Godart, C.: Ensuring Required Failure Atomicity of Composite Web Services. In: Proceedings of the 14th International World Wide Web Conference, pp. 138–147. ACM (2005)Google Scholar
  6. 6.
    Liu, A., Li, Q., Huang, L., Xiao, M.: FACTS: A Framework for Fault-tolerant Composition of Transactional Web Services. IEEE Transactions on Services Computing 3(1), 46–59 (2010)CrossRefGoogle Scholar
  7. 7.
    Harel, D., Naamad, A.: The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology 5(4), 293–333 (1996)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M.: Model Checking. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 54–56. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  9. 9.
    Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. 2, pp. 995–1072 (1990)Google Scholar
  10. 10.
    Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  11. 11.
    Ardissono, L., Goy, A., Petrone, G.: Enabling Conversations with Web Services. In: Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 819–826. ACM (2003)Google Scholar
  12. 12.
    Kova, M., Bentahar, J., Maamar, Z., Yahyaoui, H.: A Formal Verification Approach of Conversations in Composite Web Services using NuSMV. In: Proceedings of the Conference on New Trends in Software Methodologies, Tools and Techniques, pp. 245–261. IOS Press (2009)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Scott Bourne
    • 1
  • Claudia Szabo
    • 1
  • Quan Z. Sheng
    • 1
  1. 1.School of Computer ScienceThe University of AdelaideAustralia

Personalised recommendations