Proving Deadlock Freedom in Component-Based Programming

  • Paola Inverardi
  • Sebastian Uchitel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2029)


Emerging technologies such as commercial off-the-shelf products (COTS) and component integration frameworks such as CORBA and COM are changing the way software is produced. Distributed applications are being designed as sets of autonomous, decoupled components, allowing rapid development based on integration of COTS and simplifying architectural changes required to cope with the dynamics of the underlying environment. Although integration technologies and development techniques assume rather simple architectural contexts, they face a critical problem: Component integration.

So far existing techniques for detecting dynamic integration errors are based on behavioural analysis of the composed system and have serious space complexity problems. In this work we propose a broader notion of component semantics based on assumptions and a method for proving deadlock freedom in a component-based setting. Our goal is to prevent and detect these errors in component based programming settings in a component-wise fashion. We aim for effective methods that can scale to real size applications even at the price of incompleteness as opposed to many existing methods that although theoretically complete might fail in practice.


Partial Match Label Transition System Check Algorithm Component Semantic Component Behaviour 
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.


  1. 1.
    R. Alur, L. de Alfaro, T. A. Henzinger, and F. Y. C. Mang. Automatic modular verification. In Proceedings of CONCUR’ 99: Concurrency Theory, 1999.Google Scholar
  2. 2.
    F. Arbab, F.S. de Boer, and M. M. Bonsangue. A logical interface description language for components. In COORDINATION’00, vol. 1906 of LNCS. Springer, 2000.Google Scholar
  3. 3.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L.J. Hwang. Symbolic model checking: 1020 and beyond. Information and Computation, 98:142–170, June 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: a semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 15(1):36–72, January 1993.CrossRefGoogle Scholar
  5. 5.
    D. Garlan, R. Allen, and J. Ockerbloom. Architectural mismatch: Why reuse is so hard. IEEE Software, 12(6), November 1995.Google Scholar
  6. 6.
    D. Giannakopoulou, J. Kramer, and S.C. Cheung. Analysing the behaviour of distributed systems using tracta. Automated Software Engineering, 6(1):7–35, 1999.CrossRefGoogle Scholar
  7. 7.
    S. Graf, B. Steffen, and G. Luttgen. Compositional minimisation of finite state systems using interface specifications. Formal Aspects of Computing, 8(5), 1998.Google Scholar
  8. 8.
    P. Inverardi and S. Uchitel. Proving deadlock freedom in component-based programming. Technical report, Universita’ dell’Aquila, Italia, October 1999.
  9. 9.
    P. Inverardi, D. Yankelevich, and A. Wolf. Static checking of systems behaviors using derived component assumptions. ACM TOSEM, 2000.Google Scholar
  10. 10.
    N. Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20(2):436–482, March 1998.CrossRefGoogle Scholar
  11. 11.
    R. Milner. Communication and Concurrency. Prentice Hall, New York, 1989.zbMATHGoogle Scholar
  12. 12.
    O. Grumberg and D.E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, May 1994.CrossRefGoogle Scholar
  13. 13.
    R. Paige and R.E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Clemens Szyperski. Component Software. Beyond Object Oriented Programming. Addison Wesley, Harlow, England, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Paola Inverardi
    • 1
  • Sebastian Uchitel
    • 2
  1. 1.Dip. di MatematicaUniversit’a dell’ AquilaL’AquilaItaly
  2. 2.Dep. of ComputingImperial CollegeLondonUK

Personalised recommendations