Declarative specification of software architectures

Scaling formal methods to large, complex systems requires methods of modeling systems at high levels of abstraction. In this paper, we describe such a method for specifying system requirements at the software architecture level. An architecture represents a way of breaking down a system into a set of interconnected components. We use architecture theories to specify the behavior of a system in terms of the behavior of ifs components via a collection of axioms. The axioms describe the effects and limits of component variation and the assumptions a component can make about the environment provided by the architecture. As a result of the method, the verification of the basic architecture can be separated from the verification of the individual component instantiations. We present an example of using architecture theories to model the task coordination architecture of a multi-threaded plan execution system.