Automatic Checking of Component Protocols in Component-Based Systems

  • Wolf Zimmermann
  • Michael Schaarschmidt
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4089)


We statically check whether each component in a component-based system is used according to its protocol and provide counterexamples if such a check fails. The protocol is given by a finite state machine specifying legal sequences of procedure calls of the interface of a component. The main contribution is that we can deal with call-backs without any restrictions. We achieved this by using context-free grammars instead of finite state machines to describe the use of components.


State Machine Model Check Regular Language Recursive Call Procedure Call 
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.
    Attiogbé, C., André, P., Ardourel, G.: Checking Component Composability. In: Löwe, W., Südholt, M. (eds.) SC 2006. LNCS, vol. 4089, pp. 18–33. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Allen, R., Garlan, S.: A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology 6(3), 213–249 (1997)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 207–220. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Assmann, U.: Invasive Software Composition. Springer, Heidelberg (2003)zbMATHGoogle Scholar
  5. 5.
    Benedikt, M., Godefroid, P., Reps, T.: Model checking of unrestricted hierarchical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 652–666. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Bouajjani, A., Esparza, J., Finkel, A., Maler, O., Rossmanith, P., Willems, B., Wolper, P.: An efficient automata approach to some problems on context-free grammars. Information Processing Letters 74(5-6), 221–227 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)Google Scholar
  8. 8.
    Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123–137. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  9. 9.
    Burkart, O., Steffen, B.: Pushdown processes: Parallel composition and model checking. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 98–113. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  10. 10.
    Chambers, C.: Predicate classes. In: Nierstrasz, O. (ed.) ECOOP 1993. LNCS, vol. 707, pp. 268–296. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  11. 11.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Freudig, J., Löwe, W., Neumann, R., Trapp, M.: Subtyping of context-free classes. In: Proceedings 3rd White Object Oriented Nights (1998)Google Scholar
  13. 13.
    Schmidt, H.W., Krämer, B.J., Poernemo, I., Reussner, R.: Predictable component architectures using dependent finite state machines. In: Wirsing, M., Knapp, A., Balsamo, S. (eds.) RISSEF 2002. LNCS, vol. 2941, pp. 310–324. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Hind, M., Burke, M., Carini, P., Choi, J.-D.: Interprocedural pointer alias analysis. ACM Transactions on Programming Languages and Systems 21(4), 848–894 (1999)CrossRefGoogle Scholar
  15. 15.
    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation, 2nd edn. Addison-Wesley, Reading (2001)zbMATHGoogle Scholar
  16. 16.
    Kiczales, G., Lamping, J., Mendhekar, 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
  17. 17.
    Löwe, W., Neumann, R., Trapp, M., Zimmermann, W.: Robust dynamic exchange of implementation aspects. In: TOOLS 29 – Technology of Object-Oriented Languages and Systems, pp. 351–360. IEEE, Los Alamitos (1999)CrossRefGoogle Scholar
  18. 18.
    Nierstrasz, O.: Regular types for active objects. In: OOPSALA 1993. ACM SIGPLAN Notices, vol. 28 (1993)Google Scholar
  19. 19.
    Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 83–94. ACM Press, New York (2002)CrossRefGoogle Scholar
  20. 20.
    Reussner, R.H.: Counter-constraint finite state machines: A new model for resource-bounded component protocols. In: Grosky, W.I., Plášil, F. (eds.) SOFSEM 2002. LNCS, vol. 2540, pp. 20–40. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    Salomaa, A.K.: Formal Languages. Springer, Heidelberg (1978)Google Scholar
  22. 22.
    Tenzer, J., Stevens, P.: Modelling recursive calls with UML state diagrams. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 135–149. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  23. 23.
    Zimmermann, W., Schaarschmidt, M.: Model checking of client-component conformance. In: 2nd Nordic Conference on Web-Services, Mathematical Modelling in Physics, Engineering and Cognitive Sciences, vol. 008, pp. 63–74 (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Wolf Zimmermann
    • 1
  • Michael Schaarschmidt
    • 2
  1. 1.Institut für InformatikMartin-Luther Universität Halle-WittenbergHalle/SaaleGermany
  2. 2.Martin-Luther Universität Halle-Wittenberg, RechenzentrumHalle/SaaleGermany

Personalised recommendations