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

Karthikeyan Bhargavan, Carl Gunter, Elsa Gunter, Michael Jackson, Davor Obradovic, Pamela Zave

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationTheorem Proving in Higher Order Logics - 11th International Conference, TPHOLs 1998, Proceedings
EditorsJim Grundy, Malcolm Newey
PublisherSpringer-Verlag
Pages49-66
Number of pages18
ISBN (Print)3540649875, 9783540649878
StatePublished - Jan 1 1998
Externally publishedYes
Event11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998 - Canberra, Australia
Duration: Sep 27 1998Oct 1 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1479
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998
CountryAustralia
CityCanberra
Period9/27/9810/1/98

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The village telephone system: A case study in formal software engineering'. Together they form a unique fingerprint.

Cite this