"A Verified Implementation of a Control System"
Alistair A. McEwan1 and J. C. P. Woodcock2
1University of Surrey
2University of YorkAbstract:
In this paper, a case study consisting of a plant, and associated control laws, is presented. An abstract specification of a control system governing operation of the plant is given in Hoare’s Communicating Sequential Processes (CSP). The control system is known to respect the safety properties required of the plant. Via a series of calculated, verified refinements, an implementation is developed on a Field Programmable Gate Array using Handel-C. Verification is performed using the model-checker for CSP, FDR. The result is a verified system on a chip.
“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