DocumentCode
2488763
Title
ClawZ: control laws in Z
Author
Arthan, R. ; Caseley, P. ; O´Halloran, C. ; Smith, A.
Author_Institution
Lemma 1 Ltd., UK
fYear
2000
fDate
2000
Firstpage
169
Lastpage
176
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Formal Engineering Methods, 2000. ICFEM 2000. Third IEEE International Conference on
Conference_Location
York
Print_ISBN
0-7695-0822-7
Type
conf
DOI
10.1109/ICFEM.2000.873817
Filename
873817
Link To Document