An important goal of this research was the industrial application of formal design methods, i.e., methods that have a primarily mathematical rather than empirical foundation. Design methodologies play a critical role in this process by shaping the body of knowledge designers must acquire, the skills they need to master, and the kinds of tools they might employ. Program derivation (in its many forms) was adopted as the principal venue for the study and development of formal design methods.

The investigation into formal design methods centered on the UNITY model (proposed by Chandy and Misra) and was directed towards extending the applicability of various program derivation techniques to novel design domains. Refinements of the UNITY notation and logic, new program derivation strategies, and detailed case studies were the principal technical results of this investigation. The relation between systematic (but informal) design practices and the UNITY-style specification refinement was studied in the context provided by the design of a message router.

An attempt to overcome the static features of UNITY led to the development of a highly dynamic variant called Swarm. The two models share a common proof logic but the static variables and statements of UNITY were replaced in Swarm by dynamically created tuples and transactions over tuple spaces. Swarm facilitated the introduction of formal verification and derivation techniques to tuple-based languages à la Linda and to rule-based systems à la OPS5. Several case studies involving the derivation of programs meant to execute on specific kinds of parallel or distributed architectures led to the development of an assertional-style technique for formal specification of architectural constraints and to the emergence of a new program derivation strategy that integrates specification and program refinement. Swarm was also instrumental in the study of methods for specifying and reasoning about dynamic forms of synchrony among atomic actions.