This Article 
 Bibliographic References 
 Add to: 
Architecture-Directed Refinement
April 1994 (vol. 20 no. 4)
pp. 239-258

As critical computer systems continue to grow in complexity, the task of showing that they execute correctly becomes more difficult. For this reason, research in software engineering has turned to formal methods, i.e., rigorous approaches to demonstrating the correctness of software systems. Unfortunately, the formal methods currently used in the design of concurrent systems do not provide any mechanisms for specifying and reasoning about the mapping of software to hardware. As a result, architectural constraints, even though they play an important role in the design process, are left out of the formal framework. We show how to state architectural constraints in a formal notation, how to prove that programs are allocated correctly to the underlying architecture, and how to factor architectural considerations into a program derivation process which uses a mixture of specification and program refinements. The approach is illustrated by the derivation of two related programs that solve the same problem but are designed to work on distinct architectures.

[1] M. Abadi and L. Lamport, "An Old-Fashioned Recipe for Real Time," inReal-Time: Theory in Practice, J.W. de Bakker et al., eds., Springer-Verlag, Berlin and Heidelberg, LNCS 600, 1992, pp. 1-27
[2] R. J. R. Back,Correctness Preserving Program Refinements: Proof Theory and Applications. Amsterdam: Mathematical Center Tracts, vol. 131, 1980.
[3] R. J. R. Back and R. Kurki-Suonio, "Decentralization of process nets with centralized control,"Distributed Computing, vol. 3, pp. 73-87, 1989.
[4] R. J. R. Back and K. Sere, "Stepwise refinement of parallel algorithms,"Sci. Comput. Programming, vol. 13, pp. 133-180, 1990.
[5] N. Carriero and D. Gelernter, "Linda in context,"Commun. ACM, vol. 32, pp. 444-458, Apr. 1989.
[6] K. M. Chandy and J. Misra, "Distributed simulation: A case study in design and verification of distributed programs,"IEEE Trans. Software Eng., vol. SE-5 no. 5, pp. 440-452, 1979.
[7] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.
[8] K.M. Chandy and J. Misra, "An Example of Stepwise Refinement of Distributed Programs: Quiescence Detection,"ACM Trans. Programming Languages and Systems, Vol. 8, No. 3, July 1986, pp. 326-343.
[9] H. C. Cunningham and G.-C. Roman, "A UNITY-style programming logic for a shared dataspace language,"IEEE Trans. Parallel and Distributed Syst., vol. 1, no. 3, pp. 365-376, 1990.
[10] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[11] E. P. Gribomont, "Stepwise refinement and concurrency: The finite-state case,"Science of Computer Programming. Amsterdam: North Holland, vol. 14, no. 2-3, pp. 185-228, 1990.
[12] D. Gries, "A note on a standard strategy for developing loop invariants and loops,"Science of Computer Programming. Amsterdam: North Holland, vol. 2, 1982, pp. 207-214.
[13] E. Knapp, "An exercise in formal development of parallel programs: maximum flow in graphs,"ACM Trans. Programming Languages and Syst., 12(2), pp. 203-221, Apr. 1990.
[14] L. Lamport, "The temporal logic of actions," Digital Equipment Corporation, Systems Research Center, 1991.
[15] C. Lengauer, "A methodology for programming with concurrency: The formalism," inScience of Computer Programming. Amsterdam: North-Holland, vol. 2, 1982, pp. 19-52.
[16] C. C. Morgan, "Procedures, parameters, and abstraction: Separate concerns," inScience of Computer Programming. Amsterdam: North Holland, vol. 11, 1988, pp. 17-27.
[17] A. Pentland, T. Darrell, M. Turk, and W. Huang," A simple, real-time range camera," inIEEE Comput. Soc. Conf. Comput. Vision Patt Recogn., 1989, pp. 256-261.
[18] J. M. Morris, "A theoretical basis for stepwise refinement and the programming calculus,"Science of Computer Programming, vol. 9, pp. 287-306, 1987.
[19] J. M. Morris, "Laws of data refinement,"Acta Informatica, vol. 26, pp. 287-308, 1989.
[20] G.-C. Roman and H. C. Cunningham, "Mixed programming metaphors in a shared dataspace model of concurrency,"IEEE Trans. Software Eng., vol. 16, no. 12, pp. 1361-1373, 1990.
[21] G.-C. Roman and H. C. Cunningham, "Reasoning about synchronic groups," inResearch Directions in High-Level Parallel Programming Languages, J. P. Banâtre and D. Le Métayer, Eds., Lecture Notes in Computer Science, vol. 574, Springer-Verlag, 1992, pp. 21-38.
[22] G.-C. Roman, R. F. Gamble, and W. E. Ball, "Formal derivation of rule-based programs,"IEEE Trans. Software Eng., vol. 19, no. 3, pp. 277-296, 1993.
[23] M. Staskauskas, "A formal specification and design of a distributed electronic funds-transfer network,"IEEE Trans. Comput., vol. 37, no. 12, pp. 1515-1528, 1988.
[24] N. Wirth, "Program development by stepwise refinement,"Commun. ACM, vol. 14, no. 4, pp. 221-227, Apr. 1971.

Index Terms:
parallel programming; parallel architectures; formal specification; software engineering; formal methods; correctness; concurrent systems; architectural constraints; design process; program derivation process; specification; program refinements; architecture-directed refinement
G.-C. Roman, C.D. Wilcox, "Architecture-Directed Refinement," IEEE Transactions on Software Engineering, vol. 20, no. 4, pp. 239-258, April 1994, doi:10.1109/32.277573
Usage of this product signifies your acceptance of the Terms of Use.