Designing software structures, such as architectures for component software, without the use of formal modeling and analysis is error prone; but formal modeling without automatic, interactive analysis is also error prone, and it can be tedious too. We describe a case study in which we specified key aspects of Microsoft’s Component Object Model (COM) in Alloy, a lightweight notation for expressing relational models of software structures, and analyzed it with Alcoa, a tool for rapid interactive analysis. Using Alcoa, we were able to simplify an earlier formal model of COM significantly. By quickly finding many errors as we worked, Alcoa enabled us to manipulate our model more quickly and with far greater confidence than would otherwise have been possible. Our contributions include a study on the feasibility of using Alcoa to reason about such structures; an experience with a highly interactive, tool-assisted design process; and a major refinement of a significant model of COM.
Download Full PDF Version (Non-Commercial Use)