ClawZ

---

ClawZ is a tool that translates between the Simulink graphical notation for expressing control law models and the Z notation. The first version of ClawZ was developed in the Spring of 1999. This has been refined and enhanced in the light of experience on case studies and real-life examples. The current version of CLawZ (version 1.1.7) was released in February 2004.. The development of ClawZ has been sponsored by DERA and QinetiQ .

The following documents in PostScript format give more information on ClawZ.

• ClawZ - The Semantics of Simulink Diagrams: an informal discussion of some salient features of the semantics of Simulink.
• ClawZ - Model Translator Specification: a formal definition in Z of an algorithm to translate a Simulink diagram into a Z specification.
• ClawZ - Z Library Specification: a formal specification of the signatures of the Z schemas that support the translation and of the interface those signatures present to the translator.
• ClawZ - Z Library Implementation: the complete definitions of the library schemas.
• ClawZ - Z Toolkit: definitions of functions used in the ClawZ Z library and in the Z translations of Simulink diagrams.
• ClawZ - User Guide: the user guide to the tool; this includes a simple complete worked example (including Ada code and a proof of correctness).
• ClawZ - Diagram Translator Test Cases: examples of Simulink diagrams and of the corresponding model file format.
• ClawZ - System Test and Evaluation Report: a report on the evaluation work carried out; this includes the Z translation of several of the test cases from ClawZ - Diagram Translator Test Cases.

• ClawZ: Control Laws in Z

If you are interested in obtaining ClawZ please contact Rob Arthan

Acknowledgment

Created by Rob Arthan Last updated: $Date: 2004/07/19 14:07:01 $