Kermit Protocol - Formal Specification and Verification

In his foreword to the original Kermit book, Kermit: A File Transfer Protocol (1987), Don Knuth expressed his hope that “readers of this book will be challenged to find high-level concepts and invariant relations by which various versions of the Kermit protocol can be proved correct in the mathematical sense.” In this paper, published just eight years later, the protocol is formally specified and proven correct using an evolving algebra ("ealgebra") approach:

Kermit: Specification and Verification by James K. Huggins, EECS Department, University of Michican, Ann Arbor, MI 48109-2122, huggins@umich.edu, originally published in the book, Specification and Validation Methods, ed. E. Börger, Oxford University Press, 1995.

---

The book Specification and Validation Methods is available from Oxford University Press, ISBN 0-19-853854-5. Publication date: 3 August 1995. It is no longer available from the publisher but can be ordered from Amazon.com

---

The Kermit paper is available on the Web in PostScript format. It is 40 pages long; the file is 341K in length.

CLICK HERE to view the paper with your PostScript viewer, if you have one, or to obtain it via ftp if you don't.

CLICK HERE to download a PDF version obtained from the PostScript original with ps2pdf, October 2010.

The article is reproduced with the permission of Oxford University Press.