Transitioning to rigorous software specification

Describes the first attempt to use the Z formal specification language for a deliverable Bellcore product. That first attempt involved using Z to write detailed requirements for an enhancement to an existing planning and engineering system. It is recommended that the use of formal methods at Bellcore be expanded, since the preliminary results of this trial show that existing projects can thereby obtain early and cost-effective benefits. This paper includes a brief description of formal methods and the Z specification language, a brief description of the planning and engineering project that utilized Z, a description of how the trial was carried out, and a list of lessons learned from the experience