Advertisement

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

  • Karthikeyan Bhargavan
  • Carl A. Gunter
  • Elsa L. Gunter
  • Michael Jackson
  • Davor Obradovic
  • Pamela Zave
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

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.

Keywords

Domain Knowledge Finite State Machine Reactive Module Proof Obligation Inductive Sequence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur and T.A. Henzinger. Reactive modules. In Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pages 207–218, 1996.Google Scholar
  2. 2.
    R. Alur, T.A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. Mocha: Modularity in Model Checking. To appear in the Conference on Computer Aided Verification, 1998.Google Scholar
  3. 3.
    Marco Defillers, David Griffioen, and Olaf Müller. Possibly infinite sequences in theorem provers: A comparative study. In Lecture Notes in Computer Science 1275: Proceedings of the 10th International Conference, TPHOLs '97. Springer, 1997.Google Scholar
  4. 4.
    Carl A. Gunter, Elsa L. Gunter, Michael Jackson, and Pamela Zave. A reference model for requirements and specifications. Available by request, 1998.Google Scholar
  5. 5.
    Michael Jackson and Pamela Zave. Domain descriptions. In Proceedings of the IEEE International Symposium on Requirements Engineering, pages 56–64. IEEE Computer Society Press, 1992.Google Scholar
  6. 6.
    Michael Jackson and Pamela Zave. Deriving specifications from requirements: An example. In Proceedings of the Seventeenth International Conference on Software Engineering, pages 15–24. IEEE Computer Society Press, 1995.Google Scholar
  7. 7.
    Pamela Zave and Michael Jackson. Four dark corners of requirements engineering. ACM Transactions on Software Engineering and Methodology, 6(1):1–30, January 1997.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Karthikeyan Bhargavan
    • 1
  • Carl A. Gunter
    • 1
  • Elsa L. Gunter
    • 2
  • Michael Jackson
    • 3
  • Davor Obradovic
    • 1
  • Pamela Zave
    • 3
  1. 1.University of PennsylvaniaPittsburghUSA
  2. 2.Lucent TechnologiesBell LabsMurray HillUSA
  3. 3.AT&T LaboratoriesMurray HillUSA

Personalised recommendations