Projects that have used Z Word Tools

This page lists the projects that I know about that have used or are using the Z Word Tools. If you would like to contribute information about your project, please do mail the list or contact me through my SourceForge account.

ATC

Since 2005 the tools have been used to create and maintain the specification for a large software system under development for air traffic control. There are two levels of specification, one at the overall system level and a number of specifications of individual subsystems. Some subsystems will contain hundreds of thousands of lines of code. The specifications range from under 100 pages to over 1,000 pages.

The overall specification, and each subsytem specification, consists of three documents: a data model (containing not just Z but also UML, informal text, pictures, diagrams and so on) and two operation specifications: one giving an overview of the operations organised by stimulus and the other giving more detailed specifications organised by data model package.

Each document is made up of tens of separate Word files, and a lot of these are shared across different specifications. The complete specification of the overall system and of each subsystem is typechecked as a whole, using the facilities for large specifications.

The specification was developed by a team of around a dozen people.