Engineering of Complex Computer Systems, IEEE International Conference on (2006)
Aug. 15, 2006 to Aug. 17, 2006
Ana Cavalcanti , University of York, UK
Phil Clayton , Systems Assurance Group, QinetiQ Malvern, England
The design of control systems is usually based on diagrammatic definitions of control laws. The independent use of Z and CSP to verify their implementations has been successful, even for very large applications; high levels of automation have been achieved with tools based on a theorem prover called ProofPower. We have extended this approach to integrate the use of Z and CSP using a notation called Circus; as a result, we can handle a larger set of diagrams and prove more properties of the implementation. In this paper, we show how we can reuse the existing tools and experience to provide automation in the context of the new technique. This gives us confidence in its applicability in industry.
Z, CSP, Simulink, refinement.
P. Clayton and A. Cavalcanti, "Verification of Control Systems using Circus," 11th IEEE International Conference on Engineering of Complex Computer Systems(ICECCS), Stanford, CA, 2006, pp. 269-278.