Title :
ClawZ: control laws in Z
Author :
Arthan, R. ; Caseley, P. ; O´Halloran, C. ; Smith, A.
Author_Institution :
Lemma 1 Ltd., UK
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 nonlinear dynamic inversion flight control system comprising 37 pages of diagrams, 45 pages of Z and 1200 lines of non-comment Ada
Keywords :
Ada listings; aerospace control; control engineering computing; diagrams; formal specification; software tools; specification languages; Ada; ClawZ; MathWorks; ProofPower; Simulink; Z language; control engineering tool; control law diagrams; diagrams; nonlinear dynamic inversion flight control; prototype tool; Bridges; Control engineering; Control systems; Delay; Libraries; Nonlinear control systems; Nonlinear dynamical systems; Prototypes; Specification languages;
Conference_Titel :
Formal Engineering Methods, 2000. ICFEM 2000. Third IEEE International Conference on
Conference_Location :
York
Print_ISBN :
0-7695-0822-7
DOI :
10.1109/ICFEM.2000.873817
