Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
R. Arthan , Lemma 1 Ltd
P. Caseley , DERA Malvern
C. O'Halloran , DERA Malvern
A. Smith , DERA Malvern
ClawZ is a prototype tool whose objective is to link the Simulink R control-engineering tool, from MathWorks, with the ProofPower R dialect of Z. It provides a bridge between the use of Simulink to define control law diagrams and a tool to formally prove compliance between Ada and Z. The tool has been used as part of the formal proof of a Non-linear Dynamic Inversion flight control system comprising 37 pages of diagrams, 45 pages of Z and 1200 lines of non-comment Ada.
C. O'Halloran, A. Smith, P. Caseley and R. Arthan, "ClawZ: Control Laws in Z," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 169.