Formal logic and protocol specification

Addresses the design and production of an integrated set of formally-based tools, and their use in developing and testing of a suite of communications protocol specifications: development of the tools occurred in response to the requirements of an existing communications protocol specification programme. The requirements originated from recognition of the impracticability of manually proving the specifications; in consequence, development of the tools involved close co-operation between the communications analysts, who identified the functionality required, and the logic programmers, who endeavoured to provide the desired tool. The development of the tools was also driven by a requirement for portability across a wide range of hardware, from IBM PC-ATs, to workstations and super-minis. This portability was considered necessary to support the evolution of projects, from the initial feasibility stage through to full project definition