@inproceedings{f0d237c58e14456aacc1e2744920b3dc,
title = "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.",
author = "Karthikeyan Bhargavan and Gunter, {Carl A.} and Gunter, {Elsa L.} and Michael Jackson and Davor Obradovic and Pamela Zave",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1998.; 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998 ; Conference date: 27-09-1998 Through 01-10-1998",
year = "1998",
doi = "10.1007/bfb0055129",
language = "English (US)",
isbn = "3540649875",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "49--66",
editor = "Jim Grundy and Malcolm Newey",
booktitle = "Theorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings",
address = "Germany",
}