Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Aspects of Component Software

FACS 2010: Formal Aspects of Component Software pp 106–124Cite as

Model Checking Adaptive Multilevel Service Compositions

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6921))

Abstract

In this paper we present a logic-based technique for verifying both security and correctness properties of multilevel service compositions. We define modal μ-calculus formulae interpreted over service configurations. Our formulae characterize those compositions which satisfy a non-interference property and are compliant, i.e., are both deadlock and livelock free. Moreover, we use filters as prescriptions of behavior (coercions to prevent service misbehavior) and we devise a model checking algorithm for adaptive service compositions which automatically synthesizes an adapting filter.

Work partially supported by the MIUR Project IPODS “Interacting Processes in Open-ended Distributed Systems”.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abouzaid, F., Mullins, J.: Model-checking Web Services Orchestrations using BP-calculus. Electronic Notes in Theoretical Computer Science 255, 3–21 (2009)

    Article  Google Scholar 

  2. Basciutti, T.: Model-Checking Web Services. Master’s thesis, Department of Computer Science, University Ca’ Foscari of Venice (2010)

    Google Scholar 

  3. Bernardi, G., Bugliesi, M., Macedonio, D., Rossi, S.: A Theory of Adaptable Contract-Based Service Composition. In: Proc. of International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Workshop on Global Computing Models and Technologies (GlobalComp 2008), pp. 327–334. IEEE Computer Society, Los Alamitos (2008)

    Google Scholar 

  4. Bravetti, M., Zavattaro, G.: Contract Compliance and Choreography Conformance in the Presence of Message Queues. In: Bruni, R., Wolf, K. (eds.) WS-FM 2008. LNCS, vol. 5387, pp. 37–54. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Bravetti, M., Zavattaro, G.: A Foundational Theory of Contracts for Multi-party Service Composition. Fundamenta Informaticae 89(4), 451–478 (2009)

    MATH  MathSciNet  Google Scholar 

  6. Carpineti, S., Castagna, G., Laneve, C., Padovani, L.: A Formal Account of Contracts for Web Services. In: Bravetti, M., Núñez, M., Tennenholtz, M. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 148–162. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Castagna, G., Gesbert, N., Padovani, L.: A Theory of Contracts for Web Services. In: Proc. of the annual Symposium on Principles of Programming Languages (POPL 2008), pp. 261–272. ACM press, New York (2008)

    Google Scholar 

  8. Castagna, G., Gesbert, N., Padovani, L.: A Theory of Contracts for Web Services. ACM Transactions on Programming Languages and Systems (TOPLAS) 31, 53–61 (2009)

    Article  MATH  Google Scholar 

  9. Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  10. Cleaveland, R., Sims, S.: The NCSU Concurrency Workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  11. Dai, G., Bai, X., Zhao, C.: A Framework for Model Checking Web Service Compositions Based on BPEL4WS. In: Proc. of the IEEE International Conference on e-Business Engineering (ICEBE 2007), pp. 165–172. IEEE Computer Society, Los Alamitos (2007)

    Chapter  Google Scholar 

  12. Focardi, R., Gorrieri, R.: A Classification of Security Properties for Process Algebras. Journal of Computer Security 3(1), 5–33 (1994/1995)

    Article  Google Scholar 

  13. Focardi, R., Rossi, S.: Information Flow Security in Dynamic Contexts. Journal of Computer Security 14(1), 65–110 (2006)

    Article  Google Scholar 

  14. Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proc. of the IEEE Symposium on Security and Privacy (SSP 1982), pp. 11–20. IEEE Computer Society, Los Alamitos (1982)

    Google Scholar 

  15. Kozen, D.: Results on the Propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  16. Laneve, C., Padovani, L.: The must Preorder Revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  17. Mader, A.: Modal μ-calculus, Model Checking, and Gauss Elimination. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 72–88. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  18. Milner, R.: Communication and Concurrency. Prentice Hall International Series in Computer Science, vol. 92. Prentice Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  19. Müller-Olm, M.: Derivation of Characteristic Formulae. Electronic Notes in Theoretical Computer Science 18 (1998)

    Google Scholar 

  20. Nakajima, S.: Model-Checking of Safety and Security Aspects in Web Service Flows. In: Koch, N., Fraternali, P., Wirsing, M. (eds.) ICWE 2004. LNCS, vol. 3140, pp. 488–501. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  21. Nakajima, S.: Model-Checking Behavioral Specification of BPEL Applications. Electronic Notes in Theoretical Computer Science 151, 89–105 (2006)

    Article  Google Scholar 

  22. Ryan, P., Schneider, S.: Process Algebra and Non-Interference. Journal of Computer Security 9(1/2), 75–103 (2001)

    Article  Google Scholar 

  23. Schlingloff, H., Martens, A., Schmidt, K.: Modeling and Model Checking Web Services. Electronic Notes in Theoretical Computer Science 126, 3–26 (2005)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università Ca’ Foscari, Venezia, Italy

    Sabina Rossi

Authors
  1. Sabina Rossi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. HASLab (High Assurance Software Laboratory) and Dept. of Informatics, Universidade do Minho, Campus de Gualtar, 4700-320, Braga, Portugal

    Luís Soares Barbosa

  2. Faculty of Information and Communication Technologies, Swinburne University of Technology, P.O. Box 218, 3122, Hawthorn, VIC, Australia

    Markus Lumpe

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rossi, S. (2012). Model Checking Adaptive Multilevel Service Compositions. In: Barbosa, L.S., Lumpe, M. (eds) Formal Aspects of Component Software. FACS 2010. Lecture Notes in Computer Science, vol 6921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27269-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-27269-1_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-27268-4

  • Online ISBN: 978-3-642-27269-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation