Efficient deadlock analysis of component-based software architectures

• We analyze component-based systems on the basis of architectural constraints.
• Our constraint called disjoint circular wait freedom is checkable in polynomial time.
• A polynomial-time checkable condition for deadlock-freedom is established.
• We analyze the computational complexity of verification in such constrained systems.

Component-based development (CBD) is a promising approach to master the design complexity of huge software products. In addition, knowledge about the architecture of such component systems can help in establishing important system properties, which in general is computationally hard because of the state space explosion problem. Extending previous work, we here investigate the novel class of disjoint circular wait free component systems and show how we can use the architectural information to establish a condition for the property of deadlock-freedom in polynomial time. Furthermore, we emphasize the importance of this class by showing how to transform an arbitrary system into a disjoint circular wait free one in linear time and in a property preserving way and by providing various computational complexity results. A running example is included. We use the framework of interaction systems, but our results carry over to other CBD models.