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.

Tools such as Simulink(R) are being used by engineers around the world to model and solve real problems about dynamical systems. In particular control systems are modelled graphically, simulated and then code is generated automatically. Code generated from such a tool is being proposed for use in safety critical control systems. The problem for certifiers is why should they trust such generated code? This paper describes a particular approach to solving this problem which supports review by a certifier. A small case study is presented to illustrate the approach and the technical issues involved.

Describes a notation and tool for demonstrating to a third-party certifier that software written in a subset of Ada is safe, and gives some experience of using them on real projects. The thesis underlying the design is that people write adequate code, but that they make design and implementation decisions which can conflict with each other to introduce safety problems. The usual paradigm of formally specifying and then developing and verifying the code is less cost-effective than writing the code and then abstracting it to a level that is suitable for human judgements to be made. This is because there are more people who know how to write good code than those who can write effective formal specifications. The tool processes a formal, or informal, argument that code meets its safety requirements using literate programming and concepts from the refinement calculus developed at Oxford University.