Discrete event process controller synthesis using VDM++

The paper describes approaches to the specification and design of a controller for a gas burner system using VDM⁺⁺. It defines a systematic method for interpreting declarative requirements statements in real-time temporal logic, and for the construction of abstract and concrete VDM⁺⁺ specifications which implement the formalised requirements. Timing analysis is also addressed. The central contribution of the paper is a primarily mechanical process of refinement from abstract declarative specifications of a control problem to implemented controllers in Ada95