The objective of this work is to evaluate the potential use of formal program derivation techniques in the design of critical (yet reasonable-sized) components of concurrent systems. Several technical issues will be addressed. The notion of program specification will be extended to include not only a behavior specification but also formally specified constraints, e.g., the characteristics of the target architecture. The formally stated constraints will provide additional formal guidance to the design process and will lead to the emergence of new program derivation methods. The formal component of this research will be complemented by experimentation with a number of case studies ranging from simple problems having popular appeal in the literature to real components selected in cooperation with an industrial partner. Successful use of formal derivation techniques on industrial-grade problems will require a careful blend of formal methods and practical insights. Regarding the latter, experience to date suggests two particularly promising ideas to evaluate. First, is the notion of freeing much of the design process from costly formal proofs without compromising the disciplined thinking typical of formal derivation. Second, is the idea of providing powerful visual exploration, communication, and prototyping capabilities supplied by an already developed state-of-the art program visualization facility.
