Issue No. 12 - December (1994 vol. 20)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.368135
<p>A methodology for the derivation of parallel implementations from program specifications is developed. The goal of the methodology is to decompose a program specification into a collection of module specifications via property refinement, such that each module may be implemented independently by a subprogram. The correctness of the implementation is then deduced from the correctness of the property refinement procedure and the correctness of the individual subprograms. The refinement strategy is based on identifying frequently occurring control structures such as sequential composition and iteration. The methodology is developed in the context of the UNITY logic and the UC programming language, and illustrated through the solution of diffusion aggregation in fluid flow simulations.</p>
complete computer programs; program control structures; parallel programming; formal specification; program verification; flow simulation; digital simulation; diffusion; physics computing; decompositional approach; parallel program design; program specifications; parallel implementation correctness; module specifications; frequently occurring control structures; subprograms; property refinement procedure; sequential composition; iteration; UNITY logic; UC programming language; diffusion aggregation; fluid flow simulations
A. Singh, R. Bagrodia and Y. Liu, "A Decompositional Approach to the Design of Parallel Programs," in IEEE Transactions on Software Engineering, vol. 20, no. , pp. 914-932, 1994.