The Village Telephone System: A Case Study in Formal Software Engineering

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 e ective 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 re nement based on a treatment of designated terminology, domain knowledge, requirements, speci cations, 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 speci cations 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.

• Type: Conference
• Year: 1998
• Where: TPHOL
• Authors: Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave
• Keywords: Automated Reasoning, Formal Support, Speci Cations, TPHOL 1998, Village Telephone System