Issue No.04 - April (1995 vol.21)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.385972
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.
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