ClawZ: control laws in Z
Rob Arthan, P.R. Caseley, C. O'Halloran, A.O. Smith · 2002
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.