An empirical evaluation of deadlock detection in software architecture specifications

Developing and maintaining large-scale software systems is very expensive. The concept of software architecture has recently emerged as a way to suppo rt the evolution of large-scale software systems. Several architecture desc ription languages (ADLs) have been proposed to support the specification of software architectures. However, current ADLs do not provide strong suppor t for the analysis of software architecture properties. On the other hand, various analysis tools have been developed for system analysis in the forma l verification community. In this paper, we make two contributions. First, for the tools which are applicable to the property analysis of software arc hitectures, we establish a connection between different analysis tools and the software systems modeled by architecture description languages. Second, we conduct experiments to study the performance of four different analysis tools in detecting deadlocks. Based on these experiments, we are able to c ompare the efficiency of these analysis tools in verifying certain software properties.