A comparative study of formal verification techniques for software architecture specifications

With the rapid growth of network computing, the demand for large-scale and complex software systems has increased dramatically. However, the developme nt of large-scale and complex software systems is much more difficult and e rror prone. This is due to the fact that techniques and tools for assuring the correctness and reliability of software systems lag far behind the incr easing growth in size and complexity of software systems. The concept of so ftware architecture has recently emerged as a new way to improve our abilit y to effectively construct and maintain large-scale complex software system s. The architecture based development of software systems focuses on the ar chitectural elements and their overall interconnection structure. Several A rchitectural Definition Languages (ADLs) have been proposed for specifying domain specific or general purpose architectures. On the other hand, formal verification is rapidly becoming a promising and automated method to ensur e the accuracy and correctness of software systems. In this paper, we surve y several architecture description languages and formal verification method s. We present an environment to conduct experiments to study the performanc e of five different verification tools on software architecture specificati ons. Based on these experiments, we are able to compare the efficiency of t hese verification tools in verifying certain software property.