Advertisement

A proof environment for the development of group communication systems

  • Christoph Kreitz
  • Mark Hayden
  • Jason Hickey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

Abstract

We present a theorem proving environment for the development of reliable and efficient group communication systems. Our approach makes methods of automated deduction applicable to the implementation of real-world systems by linking the Ensemble group communication toolkit to the NuPRL proof development system.

We present tools for importing Ensemble's code into NuPRL and exporting it back into the programming environment. We discuss techniques for reasoning about critical properties of Ensemble as well as verified strategies for reconfiguring the Ensemble system in order to improve its performance in concrete applications.

Keywords

Type Theory Protocol Layer Formal Reasoning Automate Deduction Display Form 
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.
    M. Archer & C. Heitmeyer. Mechanical verification of timed automata: A case study. Technical report, Naval Research Laboratory, Washington, DC, 1997.Google Scholar
  2. 2.
    W. Bibel, D. Korn, C. Kreitz, F. Kurucz, J. Otten, S. Schmitt, G. Stolpmann. A multi-level approach to program synthesis. In Seventh International Workshop on Logic Program Synthesis and Transformation, LNAI, Springer Verlag, 1998.Google Scholar
  3. 3.
    K. Birman. Building Secure and Reliable Network Applications. Manning Publishing Company and Prentice Hall, 1997.Google Scholar
  4. 4.
    K. Birman & R. van Renesse. Reliable Distributed Computing with the Isis Toolkit. IEEE Computer Society Press, 1994.Google Scholar
  5. 5.
    T. Chandra, V. Hadzilacos, S. Toueg, B. Charron-Bost. On the impossibility of group membership. 15th ACM Symposium on Principles of Distributed Computing, pp. 322–330, 1996.Google Scholar
  6. 6.
    R. Constable, et. al., Implementing Mathematics with the NuPRL proof development system. Prentice Hall, 1986.Google Scholar
  7. 7.
    D. de Rauglaudre. Camlp4 version 1.06. Institut National de Recherche en Informatique et en Automatique, 1997.Google Scholar
  8. 8.
    A. Fekete, N. Lynch, A. Shvartsman. Specifying and using a partitionable group communication service. In 16th ACM Symposium on Principles of Distributed Computing, 1997.Google Scholar
  9. 9.
    M. Gordon, R. Milner, C. Wadsworth. Edinburgh LCF: A mechanized Logic of Computation. LNCS 78, Springer Verlag, 1979.Google Scholar
  10. 10.
    O. Hafizogullari & C. Kreitz. Dead Code Elimination Through Type Inference. Technical Report TR 98-1698, Cornell University, 1998.Google Scholar
  11. 11.
    M. Hayden. Ensemble Reference Manual. Cornell University, 1996.Google Scholar
  12. 12.
    The Ensemble distributed communication system. System distribution and related information. http://www.cs.cornell.edu/Info/Projects/EnsembleGoogle Scholar
  13. 13.
    C. Kreitz. Formal mathematics for verifiably correct program synthesis. Journal of the IGPL, 4(1):75–94, 1996.zbMATHMathSciNetGoogle Scholar
  14. 14.
    C. Kreitz. Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR97-1637, Cornell University, 1997.Google Scholar
  15. 15.
    C. Kreitz, J. Otten, S. Schmitt. Guiding Program Development Systems by a Connection Based Proof Strategy. In 5th International Workshop on Logic Program Synthesis and Transformation, LNCS 1048, pp. 137–151. Springer Verlag, 1996.Google Scholar
  16. 16.
    X. Leroy. The Objective Caml system release 1.06. Institut National de Recherche en Informatique et en Automatique, 1997.Google Scholar
  17. 17.
    N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.Google Scholar
  18. 18.
    P. Lincoln & J. Rushby. A formally verified algorithm for interactive consistency under a hybrid fault model. In 23rd Fault-Tolerant Computing Symposium, pp. 402–411, 1993.Google Scholar
  19. 19.
    J. Rushby. Formal methods for dependable real-time systems. In International Symposium on Real-Time Embedded Processing for Space Applications, pp. 355–366, 1992.Google Scholar
  20. 20.
    J. Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. In Dependable Computing for Critical Applications: 6, pp. 191–210. IEEE Computer Society, 1997.Google Scholar
  21. 21.
    R. van Renesse, K. Birman, & S. Maffeis. Horus: A flexible group communication system. Communications of the ACM, 39(4):76–83, 1996.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Christoph Kreitz
    • 1
  • Mark Hayden
    • 1
  • Jason Hickey
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations