Specification of software controlling a discrete-continuous environment

Abstract

In this paper, we present an object-oriented approach to the specification of discrete software controllers that are embedded in discrete-continuous (or hybrid) environments. The structure of the controller and its environment is specified using object notations extended to include continuous and hybrid objects. Control behavior is specified with state automata and pre/postconditions using the statechart notation and constructive Z-schemata. The behavior of the environment is specified '\\ith systems of differential equations using an object-oriented extension of Z for the specification of hybrid systems. We use a case study on control of a high-pressure steam boiler to illustrate how the environment structure can help to design the controller and how environment simulation can be used to derive control parameters.