The Specification and Refinement of an Environmental Model
When specifying a reactive system, we need to consider both the system itself, and the environment it operates in. A suitable formalism for such a task is the Event Calculus, a theory of synchronised state machines which lends itself to diagrammatic representation and which can be conveniently formulated in Z. In this paper we describe an approach to behavioural refinement in the Event Calculus, We consider a gas burner, starting with an outline description of its physical behaviour, then refining this by adding additional details and constraints. Each refinement step is achieved by adding a new (and simple) state machine to our existing model.