This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model
April 1995 (vol. 21 no. 4)
pp. 373-386
We are exploring an approach to formally specifying and analyzing software architectures that is based on viewing software systems as chemicals whose reactions are controlled by explicitly stated rules. This powerful metaphor was devised in the domain of theoretical computer science by Ban\^ atre and Le Mtayer and then reformulated as the Chemical Abstract Machine, or CHAM, by Berry and Boudol. The CHAM formalism provides a framework for developing operational specifications that does not 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 multiphase compiler.

[1] R. Allen and D. Garlan,“A formal approach to software architectures,”inProceedings of the IFIP Congress. New York: Elsevier, Sept. 1992.
[2] ——,“Formalizing architectural connection,”inProc. Sixteenth Int. Conf. Software Eng., 1994.
[3] J.-P. Bantre and D. Le Mtayer,“The gamma model and its discipline of programming,”Sci. Comput. Programming, vol. 15, pp. 55–77, 1990.
[4] ——,“Programming by multiset transformation,”Commun. ACM, vol. 36, no. 1, pp. 98–111, Jan. 1993.
[5] G. Berry and G. Boudol,“The chemical abstract machine,”Theoretical Comput. Sci., vol. 96, pp. 217–248, 1992.
[6] G. Boudol,“Some Chemical Abstract Machines,”inA Decade of Concurrency. New York: Springer-Verlag, in Lecture Notes in Computer Science, no. 803 pp. 92–123. May 1994.
[7] R. Potasman, J. Lis, A. Nicolau, and D. Gajski, "Percolation Based Scheduling," Proc. ACM/IEEE Design Automation Conf., pp. 444-449, 1990.
[8] D. Garlan and D. Notkin,“Formalizing design spaces: Implicit Invocation mechanisms,”inProc. VDM '91: Formal Software Development Methods, Oct. 1991.
[9] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[10] J. W. Klop and R. C. de Vrijer.Term Rewriting Systems.Cambridge, England: Cambridge University Press, to be published.
[11] P. Landin,“The mechanical evaluation of expressions,”Comput. J., vol. 6, pp. 308–320, 1964.
[12] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[13] D.L. Parnas, "On the Criteria to be Used in Decomposing Systems into Software Modules," Comm. ACM, Dec. 1972, pp. 1,053-1,058.
[14] D. E. Perry and A. L. Wolf,“Foundations for the study of software architecture,”inACM SIGSOFT Software Eng. Notes, Oct. 1992, vol. 17, no. 4, pp. 40–52.
[15] G. Plotkin,“A structural approach to operational semantics,”Univ. Aarhus, Tech. Rep. DAIMI FN–19, 1981.
[16] J. M. Spivey,The Z Notation: A Reference Manual. Englewood Cliffs, NJ: Prentice-Hall, 1989.
[17] ——,Understanding Z: A Specification Language and its Formal Semantics. Cambridge, England: Cambridge University Press, 1989.

Index Terms:
Software architecture, chemical abstract machine, specification, analysis, formal methods
Citation:
Paola Inverardi, Alexander L. Wolf, "Formal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model," IEEE Transactions on Software Engineering, vol. 21, no. 4, pp. 373-386, April 1995, doi:10.1109/32.385973
Usage of this product signifies your acceptance of the Terms of Use.