Professor of Computer Science


An important goal of my research has been 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. In my group, we viewed program derivation (in its many forms) as the principal venue for the study and development of formal design methods. Because we wanted to bridge formal studies and industrial practice, we explored program derivation techniques that were amenable to both formal and semi-formal application. Because we sought to uncover and understand fundamental issues facing concurrent systems design, the models we employed exhibit parsimony and extensions to these models were kept to a minimum.

Our 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 have been 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.

In an attempt to overcome the static features of UNITY we developed 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.

Farris Engineering
Room 301G
Ph: (505) 277-6967
Fax: (505) 277-6927
Faculty page