Skip to main content
SpringerLink
Log in

Static Verification of Indirect Data Sharing in Loosely-coupled Component Systems

  • Conference paper
Software Composition (SC 2006)

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

Included in the following conference series:

Abstract

To maintain loose coupling and facilitate dynamic composition, components in a pipe-and-filter architecture have a very limited syntactic interface and often communicate indirectly by means of a shared data repository. This severely limits the possibilities for compile time compatibility checking. Even static type checking is made largely irrelevant due to the very general types given in the interfaces. The combination of pipe-and-filter and a shared data repository is widely used, and in this paper we study this problem in the context of the Struts framework. We propose simple, but formally specified, behavioural contracts for components in such frameworks and show that automated formal verification of certain semantical compatibility properties is feasible. In particular, our verification guarantees that indirect data sharing through the shared data repository is performed consistently.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Shaw, M., Garlan, D.: Software Architecture - Perspectives on an emerging discipline. Prentice-Hall, Englewood Cliffs (1996)

    Google Scholar 

  2. Java Servlet Technology, http://java.sun.com/products/servlet/

  3. The Struts Framework, http://jakarta.apache.org/struts/

  4. The Java Modeling Language (JML), http://www.jmlspecs.org/

  5. GatorMail WebMail, http://sourceforge.net/projects/gatormail/

  6. J2EE platform specification, http://java.sun.com/j2ee/

  7. Seshadri, G.: Understanding JavaServer Pages Model 2 architecture, http://www.javaworld.com/javaworld/jw-12-1999/jw-12-ssj-jspmvc.html

  8. Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)

    Google Scholar 

  9. Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212–232 (2005)

    Google Scholar 

  10. KindSoftware: The Extended Static Checker for Java version 2 (ESC/Java2), http://secure.ucd.ie/products/opensource/ESCJava2/

  11. Leino, K.R.M., Nelson, G., Saxe, J.B. ESC/Java User’s Manual

    Google Scholar 

  12. Cok, D.R: ESC/Java2 Implementation Notes

    Google Scholar 

  13. Desmet, L., Piessens, F., Joosen, W., Verbaeten, P.: Dependency analysis of the Gatormail webmail application. Report CW 427, Department of Computer Science, K.U.Leuven, Leuven, Belgium (2005)

    Google Scholar 

  14. Desmet, L., Piessens, F., Joosen, W., Verbaeten, P.: Static verification of composition properties, http://www.cs.kuleuven.be/~lieven/research/SC2006/

  15. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06-rev28, Iowa State University, Department of Computer Science (2005)

    Google Scholar 

  16. Medvidovic, N., Taylor, R.N.: A classification and comparison framework for software architecture description languages. IEEE Trans. Softw. Eng. 26(1), 70–93 (2000)

    Article  Google Scholar 

  17. Inverardi, P., Tivoli, M.: Automatic synthesis of deadlock free connectors for com/dcom applications. In: Proceedings of the 8th ESEC held jointly with 9th ACM SIGSOFT FSE, pp. 121–131. ACM Press, New York (2001)

    Chapter  Google Scholar 

  18. Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213–249 (1997)

    Article  Google Scholar 

  19. Ivers, J., Sinha, N., Wallnau, K.: A Basis for Composition Language CL. Technical Report CMU/SEI-2002-TN-026, SEI, Carnegie Mellon University (2002)

    Google Scholar 

  20. Achermann, F., Nierstrasz, O.: Applications = Components + Scripts — A Tour of Piccola. In: Aksit, M. (ed.) Software Architectures and Component Technology, pp. 261–292. Kluwer Academic Publishers, Dordrecht (2001)

    Google Scholar 

  21. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  22. Smans, J., Jacobs, B., Piessens, F.: Static verification of code access security policy compliance of .NET applications. Journal of Object Technology 5(3) (2006)

    Google Scholar 

  23. Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, pp. 137–146. IEEE Computer Society, Los Alamitos (2005)

    Chapter  Google Scholar 

  24. Pavlova, M., Barthe, G., Burdy, L., Huisman, M., Lanet, J.L.: Enforcing high-level security properties for applets. In: CARDIS, pp. 1–16 (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DistriNet Research Group, Department of Computer Science, Katholieke Universiteit Leuven, Celestijnenlaan 200A, B-3001, Leuven, Belgium

    Lieven Desmet, Frank Piessens, Wouter Joosen & Pierre Verbaeten

Authors
  1. Lieven Desmet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank Piessens
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wouter Joosen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Pierre Verbaeten
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Software Technology Group, MSI, Växjö University, Sweden

    Welf Löwe

  2. EMN-INRIA, LINA, Dépt. Informatique, École des Mines de Nantes, OBASCO project, 4 rue Alfred Kastler, 44307, Nantes cédex 3, France

    Mario Südholt

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Desmet, L., Piessens, F., Joosen, W., Verbaeten, P. (2006). Static Verification of Indirect Data Sharing in Loosely-coupled Component Systems. In: Löwe, W., Südholt, M. (eds) Software Composition. SC 2006. Lecture Notes in Computer Science, vol 4089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11821946_3

Download citation

  • DOI: https://doi.org/10.1007/11821946_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37657-6

  • Online ISBN: 978-3-540-37659-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation