
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
G.C. Roman, C.D. Wilcox, "ArchitectureDirected Refinement," IEEE Transactions on Software Engineering, vol. 20, no. 4, pp. 239258, April, 1994.  
BibTex  x  
@article{ 10.1109/32.277573, author = {G.C. Roman and C.D. Wilcox}, title = {ArchitectureDirected Refinement}, journal ={IEEE Transactions on Software Engineering}, volume = {20}, number = {4}, issn = {00985589}, year = {1994}, pages = {239258}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.277573}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  ArchitectureDirected Refinement IS  4 SN  00985589 SP239 EP258 EPD  239258 A1  G.C. Roman, A1  C.D. Wilcox, PY  1994 KW  parallel programming; parallel architectures; formal specification; software engineering; formal methods; correctness; concurrent systems; architectural constraints; design process; program derivation process; specification; program refinements; architecturedirected refinement VL  20 JA  IEEE Transactions on Software Engineering ER   
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 OldFashioned Recipe for Real Time," inRealTime: Theory in Practice, J.W. de Bakker et al., eds., SpringerVerlag, Berlin and Heidelberg, LNCS 600, 1992, pp. 127
[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. KurkiSuonio, "Decentralization of process nets with centralized control,"Distributed Computing, vol. 3, pp. 7387, 1989.
[4] R. J. R. Back and K. Sere, "Stepwise refinement of parallel algorithms,"Sci. Comput. Programming, vol. 13, pp. 133180, 1990.
[5] N. Carriero and D. Gelernter, "Linda in context,"Commun. ACM, vol. 32, pp. 444458, 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. SE5 no. 5, pp. 440452, 1979.
[7] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: AddisonWesley, 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. 326343.
[9] H. C. Cunningham and G.C. Roman, "A UNITYstyle programming logic for a shared dataspace language,"IEEE Trans. Parallel and Distributed Syst., vol. 1, no. 3, pp. 365376, 1990.
[10] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: PrenticeHall, 1976.
[11] E. P. Gribomont, "Stepwise refinement and concurrency: The finitestate case,"Science of Computer Programming. Amsterdam: North Holland, vol. 14, no. 23, pp. 185228, 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. 207214.
[13] E. Knapp, "An exercise in formal development of parallel programs: maximum flow in graphs,"ACM Trans. Programming Languages and Syst., 12(2), pp. 203221, 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: NorthHolland, vol. 2, 1982, pp. 1952.
[16] C. C. Morgan, "Procedures, parameters, and abstraction: Separate concerns," inScience of Computer Programming. Amsterdam: North Holland, vol. 11, 1988, pp. 1727.
[17] A. Pentland, T. Darrell, M. Turk, and W. Huang," A simple, realtime range camera," inIEEE Comput. Soc. Conf. Comput. Vision Patt Recogn., 1989, pp. 256261.
[18] J. M. Morris, "A theoretical basis for stepwise refinement and the programming calculus,"Science of Computer Programming, vol. 9, pp. 287306, 1987.
[19] J. M. Morris, "Laws of data refinement,"Acta Informatica, vol. 26, pp. 287308, 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. 13611373, 1990.
[21] G.C. Roman and H. C. Cunningham, "Reasoning about synchronic groups," inResearch Directions in HighLevel Parallel Programming Languages, J. P. Banâtre and D. Le Métayer, Eds., Lecture Notes in Computer Science, vol. 574, SpringerVerlag, 1992, pp. 2138.
[22] G.C. Roman, R. F. Gamble, and W. E. Ball, "Formal derivation of rulebased programs,"IEEE Trans. Software Eng., vol. 19, no. 3, pp. 277296, 1993.
[23] M. Staskauskas, "A formal specification and design of a distributed electronic fundstransfer network,"IEEE Trans. Comput., vol. 37, no. 12, pp. 15151528, 1988.
[24] N. Wirth, "Program development by stepwise refinement,"Commun. ACM, vol. 14, no. 4, pp. 221227, Apr. 1971.