Developing reactive systems in a VDM framework
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.
This page was built for publication: Developing reactive systems in a VDM framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685617)
