The village telephone system: A case study in formal software engineering

Abstract

In this paper we illustrate the use of formal methods in the development of a benchmark application we call the Village Telephone System which is characteristic of a class of network and telecommunication protocols. The aim is to show an effective integration of methodology and tools in a software engineering task that proceeds from user-level requirements to an implementation. In particular, we employ a general methodology which we advocate for requirements capture and refinement based on a treatment of designated terminology, domain knowledge, requirements, specifications, and implementation. We show how a general-purpose theorem prover (HOL) can provide formal support for all of these components and how a model checker (Mocha) can provide formal support for the specifications and implementation. We develop a new HOL theory of inductive sequences that is suited to modelling reactive systems and provides a common basis for interoperability between HOL and Mocha.