A proof environment for the development of group communication systems
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.
KeywordsType Theory Protocol Layer Formal Reasoning Automate Deduction Display Form
Unable to display preview. Download preview PDF.
- 1.M. Archer & C. Heitmeyer. Mechanical verification of timed automata: A case study. Technical report, Naval Research Laboratory, Washington, DC, 1997.Google Scholar
- 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.K. Birman. Building Secure and Reliable Network Applications. Manning Publishing Company and Prentice Hall, 1997.Google Scholar
- 4.K. Birman & R. van Renesse. Reliable Distributed Computing with the Isis Toolkit. IEEE Computer Society Press, 1994.Google Scholar
- 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.R. Constable, et. al., Implementing Mathematics with the NuPRL proof development system. Prentice Hall, 1986.Google Scholar
- 7.D. de Rauglaudre. Camlp4 version 1.06. Institut National de Recherche en Informatique et en Automatique, 1997.Google Scholar
- 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.M. Gordon, R. Milner, C. Wadsworth. Edinburgh LCF: A mechanized Logic of Computation. LNCS 78, Springer Verlag, 1979.Google Scholar
- 10.O. Hafizogullari & C. Kreitz. Dead Code Elimination Through Type Inference. Technical Report TR 98-1698, Cornell University, 1998.Google Scholar
- 11.M. Hayden. Ensemble Reference Manual. Cornell University, 1996.Google Scholar
- 12.The Ensemble distributed communication system. System distribution and related information. http://www.cs.cornell.edu/Info/Projects/EnsembleGoogle Scholar
- 14.C. Kreitz. Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR97-1637, Cornell University, 1997.Google Scholar
- 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.X. Leroy. The Objective Caml system release 1.06. Institut National de Recherche en Informatique et en Automatique, 1997.Google Scholar
- 17.N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.Google Scholar
- 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.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.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