On relating functional specifications to architectural specifications: A case study

Software architecture specifications are predominantly concerned with describing the component structure of systems and how the components interact behaviorally. They are increasingly part of standardized software development processes because they represent a system abstraction in which design choices relevant to the correctness of the final system are taken. Therefore, much of software architecture research has concentrated on specification and analysis, whereas little attention has been paid to formally relating architectural specifications to higher levels of specification, such as the system requirements. In this paper we present our progress toward addressing an instance of this problem, namely relating state-based software architecture specifications to high-level functional specifications. Our approach is to use an intermediate specification given in terms of a set of temporal logic properties to bridge the gap between the two levels of specifications. We describe our approach in the context of a particular case study, the AEGIS GeoServer Simulation Testbed system, showing how a compact functional specification of a critical behavioral property of the system can be used to validate three alternative architectural specifications of that system.