Using formal methods to reason about architectural standards

Abstract

We present a study in which we used formal methods to reason precisely about aspects of a widely used software architectural standard, namely Microsoft's Component Object Model (COM). We developed a formal theory of COM to help us reason about a proposed compositional architectural style based on COM, intended for use in a novel commercial multimedia authoring system. The style combined COM objects, integration mediators, and the COM reuse mechanism of aggregation. Our use of formal methods averted an architectural disaster by revealing essential but subtle and counterintuitive properties of COM. We partially validated our theory by subjecting it to review by the designers of COM and by testing it against other available data. The theory has good evidential support.