ClawZ

---

The ClawZ project produced a research prototype of a tool that translates between the Simulink graphical notation for expressing control law models and the Z notation. The project began in Spring of 1999. The ideas have since been refined and enhanced in the light of experience on case studies and real-life examples. The development of ClawZ was originally sponsored by QinetiQ . CLawZ®, the commercial successor to the prototype tool, is developed and maintained by D-RisQ.

The following documents give more information on the ClawZ research project.

• 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.

The following is a paper on ClawZ presented at ICFEM 2000:

• ClawZ: Control Laws in Z

For more information on CLawZ® and related technologies, see D-RisQ's portfolio of software tools.

Acknowledgment

Created by Rob Arthan Last updated: $Date: 2015/10/30 11:41:11 $