From FM'99, World Congress on Formal Methods.
September, 1999.

This paper describes the process of implementing an architecture for secure distributed transaction processing, the process of verifying that it has the desired security properties, and the implementation that resulted. The implementation and verification processes provided us with valuable experience relevant to answering several questions posed by our research on transformational development of architectures. To what extent can implementation-level architectural descriptions be derived from abstract description via application of transformations that preserve a broad class of properties, which includes satisfaction of various access control policies? To what extent can a formal derivation of a non-secure implementation-level distributed transaction processing architecture be reused in derivation of a secure architecture? Are the transformation verification techniques that we have developed sufficient for verifying a collection of transformations adequate for implementing complex secure architecture? Do our architecture hierarchies effectively fill the gap between abstract, intellectually manageable models of a complex architecture and the actual implementation? Exploring the answers to these questions resulted in a reference implementation of an architecture for secure distributed transaction processing, and an independently interesting demonstration instance of the reference implementation.

@inproceedings{fm99wcfm,
    AUTHOR = {{F.} Gilham and {R.} {A.} Riemenschneider and and {V.} Stavridou},
    TITLE = {Secure Interoperation of Secure Distributed Databases: An Architecture Verification Case Study},
    BOOKTITLE = {{FM'99,} World Congress on Formal Methods},
    YEAR = {1999},
    MONTH = {sep},
    URL = {http://www.sdl.sri.com/papers/fm99-2/}
}

• fm99-2.ps.gz