Using Z to Describe Large Systems

Abstract

This paper deals with the problems of using Z on a large software product. The specific aim is to show how Z can be used to describe a large system, where the number of refinement steps from a single abstract view to implementation is large, i.e. significantly more than one or two as assumed by the average textbook. The method described is currently in use for respecifying TPMS, ICL’s Transaction Processing monitor for VME.

We intend to concentrate on the design method, avoiding discussion on why we are applying it to TPMS and what the consequences might be. This could be the subject of a future paper, after we have given the method prolonged exposure and used the results on the actual product. The current paper deals with the subject from a practical point of view: it is aimed more at an audience of software designers than mathematicians.

The primary feature of the method described is that it allows for an arbitrary number of refinement steps between initial specification and implementation, without requiring that we re-describe the entire system at every level. This avoids duplication, and in so doing helps to prevent the introduction of inconsistencies between levels (given that proof of consistency is not economic). The resulting design record consists of a tree-like structure of individual specifications, each of which is complete in its own right. Each design step requires the consideration of a single specification, either as an isolated entity or as an abstract view of a small number of lower level specifications. Thus the complexity of the design task does not increase with the size of the system.

We show that despite having an arbitrary number of levels of abstraction, a design produced using this method still has four parts corresponding to the traditional Requirements — Specification — Design — Implement split, but that