Enforcing Different Contracts in Hierarchical Component-Based Systems

  • Philippe Collet
  • Alain Ozanne
  • Nicolas Rivierre
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4089)


Using different specification formalisms together is necessary to leverage better reliability on component-based systems. The ConFract system provides a contracting system for hierarchical software components, but currently, only executable assertions are supported.

In this paper, we describe how TLA, taken as an instance of behavioral sequence-based formalism, was integrated in ConFract. A domain specific language is proposed in order to enable designers to describe the observations needed to appropriately verify their specifications. These observations are automatically generated for assertions and in the case of TLA, we show what kind of observations must be provided to link the specifications to the concrete application.


Model Checker Temporal Logic Correct Behavior Execution Trace Target Speed 
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.
    Allen, R.J., Garlan, D.: A formal basis for architectural connection. ACM, Transactions on Software Engineering and Methodology 6 (July 1997)Google Scholar
  2. 2.
    Barnett, M., Schulte, W.: Runtime Verification of .NET Contracts. Journal of Systems and Software 65(3), 199–208 (2003)Google Scholar
  3. 3.
    Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Bruneton, E., Coupaye, T., Leclercq, M., Quéma, V., Stefani, J.-B.: An Open Component Model and Its Support in Java. In: Crnković, I., Stafford, J.A., Schmidt, H.W., Wallnau, K. (eds.) CBSE 2004. LNCS, vol. 3054, pp. 7–22. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Bruneton, E., Coupaye, T., Stefani, J.-B: The Fractal component model. Specification, Technical Report v1, v2, The ObjectWeb Consortium (2002/2003),
  6. 6.
    Chang, H., Collet, P.: Fine-grained Contract Negotiation for Hierarchical Software Components. In: 31th EUROMICRO Conference 2005, Porto, Portugal, 30 August - 3 September 2005. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  7. 7.
    Collet, P., Rousseau, R., Coupaye, T., Rivierre, N.: A Contracting System for Hierarchical Components. In: Heineman, G.T., Crnković, I., Schmidt, H.W., Stafford, J.A., Szyperski, C., Wallnau, K. (eds.) CBSE 2005. LNCS, vol. 3489, pp. 187–202. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Diaz, M., Juanole, G., Courtiat, J.P.: Observer – a concept for formal on-line validation of distributed systems. IEEE Trans. on Software Engineering 20(12), 900–913 (1994)CrossRefGoogle Scholar
  9. 9.
    Goldberg, A., Havelund, K.: Instrumentation of java bytecode for runtime analysis. In: Fifth ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP 2003) (July 2004)Google Scholar
  10. 10.
    Havelund, K., Roşu, G.: Efficient monitoring of safety properties. International Journal on Software Tools for Technology Transfer (STTT) 6(2), 158–173 (2004)Google Scholar
  11. 11.
    Kiczales, G., Lamping, J., Menhdhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  12. 12.
    Lamport, L.: The Temporal Logic of Actions. ACM Trans. on Programming Languages and Systems 16(3), 872–923 (1994)CrossRefGoogle Scholar
  13. 13.
    Lamport, L.: Specifying Systems: The TLA +  Language and Tools for Hardware and Software Engineers. Addison Wesley, Reading (2002)Google Scholar
  14. 14.
    Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer, Dordrecht (1999)Google Scholar
  15. 15.
    Luckham, D.C., Vera, J.: An event-based architecture definition language. IEEE Trans. Software Eng. 21(9), 717–734 (1995)CrossRefGoogle Scholar
  16. 16.
    Magee, J., Kramer, J.: Concurrency: state models & Java programs. John Wiley & Sons, Inc., Chichester (1999)zbMATHGoogle Scholar
  17. 17.
    Magee, J., Kramer, J., Giannakopoulou, D.: Behaviour analysis of software architectures. In: WICSA, pp. 35–50 (1999)Google Scholar
  18. 18.
    Medvidovic, N., Taylor, R.N.: A classification and comparison framework for software architecture description languages. IEEE Transactions on Software Engineering 26(1), 70–93 (2000)CrossRefGoogle Scholar
  19. 19.
    Meyer, B.: Applying design by contract. IEEE Computer 25, 40–51 (1992)Google Scholar
  20. 20.
    Object Management Group. Object Constraint Language Specification. Tech. Rep. version 1.1, ad/97-08-08, IBM (September 1997),
  21. 21.
    Pahl, C.: Components, contracts, and connectors for the unified modelling language UML. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 259–277. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  22. 22.
    Plasil, F.: Enhancing component specification by behavior description: the sofa experience. In: WISICT 2005: Proceedings of the 4th international symposium on Information and communication technologies, Trinity College Dublin, pp. 185–190 (2005)Google Scholar
  23. 23.
    Plasil, F., Visnovsky, S.: Behavior protocols for software components. IEEE Transactions on Software Engineering 28(11) (November 2002)Google Scholar
  24. 24.
    Richardson, D.J., Aha, S.L., O’Malley, T.O.: Specification-based test oracles for reactive systems. In: 14th International Conference on Software Engineering (ICSE 1992), pp. 105–118 (1992)Google Scholar
  25. 25.
    Rivierre, N., Horn, F., Tran, F.D.: On monitoring concurrent systems with TLA: an example. In: Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), St Malo, FR, pp. 36–47 (June 2005)Google Scholar
  26. 26.
    Szyperski, C.: Component Software — Beyond Object-Oriented Programming, 2nd edn. Addison-Wesley Publishing Co, Reading (2002)Google Scholar
  27. 27.
    TLA. References to the TLA literature,
  28. 28.
    van Deursen, A., Klint, P., Visser, J.: Domain-specific languages: An annotated bibliography. SIGPLAN Notices 35(6), 26–36 (2000)CrossRefGoogle Scholar
  29. 29.
    Weis, T., Becker, C., Geihs, K., Plouzeau, N.: A UML meta-model for contract aware components. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 442–456. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Philippe Collet
    • 1
  • Alain Ozanne
    • 2
  • Nicolas Rivierre
    • 2
  1. 1.I3S LaboratoryUniversity of Nice – Sophia AntipolisFrance
  2. 2.France Telecom R&D, MAPS/AMS LaboratoryIssy les MoulineauxFrance

Personalised recommendations