A Calculated Implementation of a Control System
Alistair A. McEwan · 2004
In this paper, a case study consisting of a plant, and associated control laws, is presented. An abstract specification of the control system is given in Hoare's Communicating Sequential Processes (CSP). Via a series of calculated refinements, an implementation is developed, and translated into a simulation in a Java-based library for CSP, JCSP. Verification of the development process is performed using the model- checker for CSP, FDR. The result is a complete, verified implementation of the control system. Control (n): The apparatus by means of which a machine, as an aeroplane or motor vehicle, is controlled during operation; also, any of the mechanisms of a control apparatus, or collectively for the complete apparatus. Oxford English Dictionary, 2nd edition In this paper, a case study consisting of a plant, and control laws, is investigated. An exe- cutable simulation of the control system is developed via a full, verified, top down procedure from an existing abstract specification. Proof obligations are discharged using FDR. The case study in question is a steam boiler—a device which accepts water input from a set of pumps, boils the water, and allows steam to escape through sets of valves. The boiler can be seen as analogous to, for instance, a cooling system in a nuclear reactor. An instantiation of the abstract control system is developed, and its correctness verified. This instantiation is then transformed into an executable refinement, and from this, a simulation is produced by translating this model into a Java-based library for CSP, JCSP. Development of the new device is done in a top-down manner. The existing abstract specification of the device is refined in several stages into models where the implementation is exposed gradually. It is our belief that, by taking an abstract specification, and using a calculational approach to refining it into a concrete model, a high level of confidence can be achieved in the correctness of the implementation. The contribution of this paper, therefore, can be summarised as a demonstration of a full top-down development technique, from a high level specification to a dependable, verified, executable program. The paper begins by presenting some relevant background material, including the case study in question. This is followed by a detailed description of the control laws in section 2. In section 3, a refinement of this model is produced, involving concrete instantiations of the processes necessary to implement the laws, and is further refined into an executable model in section 4. The executable model is translated into JCSP in section 5, resulting in a verified implementation of the abstract model. Some conclusions are drawn in section 6.