Discrete-event modelling in VDM

Abstract

The design of software controllers for embedded systems demands notations and tools that have that are able to describe systems that evolve via discrete events, and so express the structure and logic of control architectures. This chapter presented the features of VDM"an established formalism for describing discrete event systems"that support the modelling and design of controllers. These include abstract specification of data restricted by invariants, and operations that work on persistent data for specification of control functionality. Structured and collection types enable supervisory control to be modelled. Model structuring on object-oriented principles enable the description of architectural solutions to problems like safety control, and the management of concurrency. The formalism, which is implemented in the Overture and Crescendo tools, is illustrated via a series of examples based on control of a torsion bar.