FORMAL SPECIFICATION AND ANALYSIS OF SOFTWARE ARCHITECTURES USING THECHEMICAL ABSTRACT MACHINE MODEL

We are exploring an approach to formally specifying and analyzing soft ware architectures that is based on viewing software systems as chemic als whose reactions are controlled by explicitly stated rules. This po werful metaphor was devised in the domain of theoretical computer scie nce by Banatre and Le Metayer and then reformulated as the Chemical Ab stract Machine, or CHAM, by Berry and Boudol. The CHAM formalism provi des a framework for developing operational specifications that does no t bias the described system toward any particular computational model. It also encourages the construction and use of modular specifications at different levels of detail. We illustrate the use of the CHAM for architectural description and analysis by applying it to two different architectures for a simple, but familiar, software system, the multip hase compiler.