Proving Deadlock Freedom in Component-Based Programming
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.
KeywordsPartial Match Label Transition System Check Algorithm Component Semantic Component Behaviour
- 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.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
- 5.D. Garlan, R. Allen, and J. Ockerbloom. Architectural mismatch: Why reuse is so hard. IEEE Software, 12(6), November 1995.Google Scholar
- 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.P. Inverardi and S. Uchitel. Proving deadlock freedom in component-based programming. Technical report, Universita’ dell’Aquila, Italia, October 1999. http://www.doc.ic.ac.uk/su2/pubs/techrep99.pdf
- 9.P. Inverardi, D. Yankelevich, and A. Wolf. Static checking of systems behaviors using derived component assumptions. ACM TOSEM, 2000.Google Scholar
- 14.Clemens Szyperski. Component Software. Beyond Object Oriented Programming. Addison Wesley, Harlow, England, 1998.Google Scholar