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

  • Lieven Desmet
  • Frank Piessens
  • Wouter Joosen
  • Pierre Verbaeten
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4089)


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.


Frame Condition Action Contract Java Modeling Language Indirect Data Composition Property 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Shaw, M., Garlan, D.: Software Architecture - Perspectives on an emerging discipline. Prentice-Hall, Englewood Cliffs (1996)Google Scholar
  2. 2.
    Java Servlet Technology,
  3. 3.
    The Struts Framework,
  4. 4.
    The Java Modeling Language (JML),
  5. 5.
  6. 6.
    J2EE platform specification,
  7. 7.
    Seshadri, G.: Understanding JavaServer Pages Model 2 architecture,
  8. 8.
    Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)Google Scholar
  9. 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. 10.
    KindSoftware: The Extended Static Checker for Java version 2 (ESC/Java2),
  11. 11.
    Leino, K.R.M., Nelson, G., Saxe, J.B. ESC/Java User’s ManualGoogle Scholar
  12. 12.
    Cok, D.R: ESC/Java2 Implementation NotesGoogle Scholar
  13. 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. 14.
    Desmet, L., Piessens, F., Joosen, W., Verbaeten, P.: Static verification of composition properties,
  15. 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. 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)CrossRefGoogle Scholar
  17. 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)CrossRefGoogle Scholar
  18. 18.
    Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213–249 (1997)CrossRefGoogle Scholar
  19. 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. 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. 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)CrossRefGoogle Scholar
  22. 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. 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)CrossRefGoogle Scholar
  24. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Lieven Desmet
    • 1
  • Frank Piessens
    • 1
  • Wouter Joosen
    • 1
  • Pierre Verbaeten
    • 1
  1. 1.DistriNet Research Group, Department of Computer ScienceKatholieke Universiteit LeuvenLeuvenBelgium

Personalised recommendations