This project attacks the process control problems using a formal method for program derivation that is based on Hoare-style proof outlines. This involves investigations into formal methods for reasoning about real-time and fault-tolerance. It also involves applying the resulting methodology to actual process control problems, leading to improved notations and techniques for suppressing irrelevant details when deriving moderate-sized concurrent and distributed programs.