An empirical evaluation of deadlock detection in software architecture specifications

Abstract

Developing and maintaining large-scale software systems is very expensive. The concept of software architecture has recently emerged as a way to support the evolution of large-scale software systems. Several architecture description languages (ADLs) have been proposed to support the specification of software architectures. However, current ADLs do not provide strong support for the analysis of software architecture properties. On the other hand, various analysis tools have been developed for system analysis in the formal verification community. In this paper, we make two contributions. First, for the tools which are applicable to the property analysis of software architectures, 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 compare the efficiency of these analysis tools in verifying certain software properties.