This paper explores the combination of formal methods with techniques taken from control engineering for specifying, designing and verifying reactive systems.
In particular, it is shown how to use techniques for specification and verification in VDM++ in combination with the synthesis of procedural controllers, a mathematical abstraction of the logic controlling an eventdriven sequential operation. The procedural controller is used as a provably correct specification of an event-driven operation to be implemented using VDM++. The resulting method enables a systematic approach for creating formalized designs of controllers for this type of operations, and proof obligations for the correctness of the designs against specifications to be generated. The approach is illustrated using an example.