This research project investigates methods for the systematic development of concurrent programs, focusing upon formal methods for specification, derivation, and refinement. The project defines a taxonomy of program development methods and uses it to classify and study the existing methods. Building on this study, the research is synthesizing new methods which merge the strong features of the existing methods with promising new techniques. The project uses several carefully chosen case studies to evaluate and refine these new methods and then adapts the new methods to several different concurrent programming models. This work is showing new ways that existing theory and methods can be put into practice. It also has the potential for uncovering significant new formal methods for the development of concurrent programs. The research may also reveal the possibility of innovative software engineering tools and educational techniques.
