The Community for Technology Leaders
Formal Engineering Methods, International Conference on (2000)
York, England
Sept. 4, 2000 to Sept. 7, 2000
ISBN: 0-7695-0822-7
pp: 169
R. Arthan , Lemma 1 Ltd
P. Caseley , DERA Malvern
C. O'Halloran , DERA Malvern
A. Smith , DERA Malvern
ABSTRACT
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.
INDEX TERMS
CITATION

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.
doi:10.1109/ICFEM.2000.873817
89 ms
(Ver 3.3 (11022016))