Developing reactive systems in a VDM framework (Q685617)

The paper studies the detailed development of reactive systems, using an extension of VDM. The extension allows specification and proof of behavioural aspects to be expressed in the VDM framework. The development of a reactive system starts from a state machine description of its environment. This description is then translated into VDM to provide a context for the specification of the reactive system itself. The reactive system and its environment are then seen as a single closed system. Traces of the input-output activities are used to model interactions. Moreover, a distinction is introduced between external entities (the environment), internal entities (the reactive system under development) and interface entities. A series of axioms and inference rules is added to VDM to take the notions of external entities and traces into account. These extensions are illustrated by the development of a case study: the vending machine. The paper presents the specification of the case study and outlines the major design steps. The actual proof of the case study was led into sufficient detail to allow its verification by a theorem prover. One of the major objectives of this work is to improve the understanding of the practical implications of the specification, design, and symbolic validation of machine-checked reactive systems.