This Article 
 Bibliographic References 
 Add to: 
Correct Architecture Refinement
April 1995 (vol. 21 no. 4)
pp. 356-3
A method is presented for the stepwise refinement of an abstract architecture into a relatively correct lower level architecture that is intended to implement it. A refinement step involves the application of a predefined refinement pattern that provides a routine solution to a standard architectural design problem. A pattern contains an abstract architecture schema and a more detailed schema intended to implement it. The two schemas usually contain very different architectural concepts (from different architectural styles). Once a refinement pattern is proven correct, instances of it can be used without proof in developing specific architectures. Individual refinements are compositional, permitting incremental development and local reasoning. A special correctness criterion is defined for the domain of software architecture, as well as an accompanying proof technique. A useful syntactic form of correct composition is defined. The main points are illustrated by means of familiar architectures for a compiler. A prototype implementation of the method has been used successfully in a real application.

[1] M. Abadi and L. Lamport,“Composing specifications,”ACM Trans. Programming Languages and Syst., vol. 15, no. 1, pp. 73–132, Jan. 1993.
[2] ——,“Conjoining specifications,”Digital Syst. Res. Cen., Palo Alto, CA, Tech. Rep. 118, Dec. 1993.
[3] ——,“Formalizing architectural connection,”inProc. Sixteenth Int. Conf. Software Eng., 1994.
[4] E. Brinksma, B. Jonsson and F. Orava,“Refining interfaces of communicating systems,”inTAPSOFT '91:, Lecture Notes in Computer Science 494, S. Abramsky and T. S. E. Maibaum, Eds. New York: Springer-Verlag, 1991, pp. 297–312.
[5] M. Broy,“Compositional refinement of interactive systems,”Digital Syst. Res. Cen., Palo Alto, CA, Tech. Rep. no. 89, July 1992.
[6] H. B. Enderton,A Mathematical Introduction to Logic. New York: Academic, 1972.
[7] T. DeMarco,Structured Analysis and System Specification. New York: Yourdan, 1979.
[8] D. Garlan et al., "Exploiting Style in Architectural Design Environments," ACM SIGSOFT, pp. 175-188, 1994.
[9] D. Garlan and M. Shaw,“An introduction to software architecture,”inAdvances in Software Engineering and Knowledge Engineering, Vol. 1, V. Ambriola and G. Tortora, Eds., World Scientific Publishing Company, 1993.
[10] S. L. Gerhart,“Knowledge about programs,”inProc. Int. Conf. Software Reliability, Los Angeles, CA, Apr. 1975, pp. 88–95.
[11] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[12] ——,“Proof of correctness of data representations,”Acta Informatica, vol. 1, no. 4, pp. 271–281, 1972.
[13] M. A. Jackson,Principles of Program Design. New York: Academic, 1975.
[14] D. Katiyar,D. Luckham,, and J. Mitchell,“A type system for prototyping languages,” Proc. 21st ACM Symp. on Principles of Programming Languages, Portland, 1994.
[15] D.C. Luckham,J. Vera,D. Bryan,L. Augustin,, and F. Belz,“Partial orderings of event sets and their application toprototyping concurrent, timed systems,” J. of Systems and Software, vol. 21, no. 3, pp. 253-265, June 1993.
[16] G. R. McClain, Ed.,Open Systems Interconnection Handbook. New York: McGraw-Hill, 1991.
[17] M. Moriconi and D. F. Hare,“The PegaSys system: Pictures as formal documentation of large programs,”ACM Trans. Programming Languages and Syst., vol. 8, no. 4, pp. 524–546, Oct. 1986.
[18] M. Moriconi and X. Qian, "Correctness and Composition of Software Architectures," ACM SIGSOFT '94, 1994.
[19] R. Reiter,“Deductive question-answering on relational databases,”inLogic and Data Bases, H. Gallaire and J Minker, Eds. New York: Plenum, 1978, pp. 149–177.
[20] E. Yourdon and L. Constantine, Structured Design: Fundamentals of a Discipline of Computer Program and Systems Design.Englewood Cliffs, N.J.: Prentice Hall, 1979.

Index Terms:
Software architecture, hierarchy, stepwise refinement, refinement patterns, formal methods, relative correctness, composition
Mark Moriconi, Xiaolei Qian, R. A. Riemenschneider, "Correct Architecture Refinement," IEEE Transactions on Software Engineering, vol. 21, no. 4, pp. 356-3, April 1995, doi:10.1109/32.385972
Usage of this product signifies your acceptance of the Terms of Use.