Applying static analysis to software architectures

In this paper we demonstrate how static concurrency analysis techniques can be used to verify applicationspecic properties of an architectural description Specically we use two concurrency anal ysis tools INCA a ow equation based tool and FLAVERS a data ow analysis based tool to detect errors or prove properties of a Wright architectural description of the gas station problem Although both these tools are research prototypes they illustrate the potential of static analysis for verifying that architectural descriptions adhere to important properties for detecting problems early in the lifecycle and for helping developers understand the changes that need to be made to satisfy the properties being analyzed With the advent of improved network technology distributed systems are becoming increasingly common Such systems are more dicult to reason about than sequential systems because of their inherent nondeter minism In recognition of this software architecture research is attempting to dene architectural languages to help developers describe distributed system designs These highlevel descriptions allow developers to f