The benefits of formal specification are not automatic

It is often claimed that the use of formal specification languages gives rise to the desirable properties of clarity and abstraction in specifications, and that their use leads to the early detection of ambiguity and inconsistencies in requirements. This paper reports on a case study in the use of Z to specify the software functionality of a subsystem in a hard real-time application (a missile system) where each of these benefits failed to follow automatically from producing the Z specification. The reasons why these benefits failed to materialise are discussed, and it is concluded that although formal notations can give rise to these benefits, they are harder to realise in real-time embedded software than the `data-processing´ systems often used as examples in academic papers