This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Citation:
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.