Architectural definition often begins with a very high level architectural description, e.g., specification of dataflow among a few abstract components. This high level description is then refined in order to ultimately achieve a much more detailed description that can be implemented directly. On the other hand, with the ad vent of the object-oriented paradigm, architectural definition can consist of assembling a collection of standard components and connectors. But, if such an assemblage is complex, it is desirable to generate more abstract descriptions from it, in order to facilitate understand ing and analysis. In either case, the end product of the architecting process is an architectural hierarchy, a collection of architectural descriptions linked by map pings that interpret the more abstract descriptions in the more concrete descriptions.

Formalized transformational approaches to architecture refinement and abstraction have been proposed. One argument in favor of formalization is that it can result in architectural implementations that are guaranteed to be correct, relative to the abstract descriptions. If an abstract description and an implementation are correct with respect to one another, conclusions obtained by reasoning from an abstract architectural description will apply to the implemented architecture as well. But this correctness guarantee is achieved by requiring that the implementor use only verified transformations, Le., transformations that have been proven to produce correct results whenever they are applied.

This paper explores an approach to allowing the implementor the freedom to use transformations that have not been proven to be generally correct, without voiding the correctness guarantee. Checking means determining that application of the transformation produced the de sired result by performing a straightforward calculation of some sort. Checking allows the use of transformations that have not been generally verified, even transformations that are known to sometimes produce incorrect results, by showing that they work in the particular case.

Our initial approach to checking, inspired by Necula and Lee's work on certifying compilers, involves check ing that these non-verified transformation steps preserve proofs of the critical properties of interest, such as system security. This approach will be illustrated by an example drawn from our research on architectures for secure distributed transaction processing. Other approaches, useful for checking that broad classes of properties are preserved by the transformation step, are also being investigated.

Although the primary objective of this work is to al low the architect greater flexibility in correctly implementing abstract architectures and generating accurate abstract views of architectures, it has other benefits as well. For example, because verification is a more complex and error-prone process than checking, a combination of verification and checking particular refinement steps can substantially increase confidence that an abstract description correctly characterizes an implementation.

• pca.ps