Abstract
The MITRE Corporation has pursued formal methods research and applications over many years. We have found that applying formal methods to a mathematical description at the algorithm level, using ordinary rigorous mathematical methods for proofs, leads to a high level of insight. We discuss three main projects as illustrations. The first produced specifications for the TCP protocol using CSP and state machine methods. The protocol was proved to provide reliable delivery. In the second, we used IMPS, an Interactive Mathematical Proof System, to prove the correctness of a state machine refinement justifying a simple virtual memory scheme. This exercise was part of an effort to provide assurance for the virtual memory system within the Mach microkernel. In the third, called VLISP, we developed a verified implementation of the Scheme programming language, the first for any programming language in widespread use. The techniques we devised can be re-used to verify a wide range of sequential programs.
The work described in this note was funded by the United States Air Force ESC under contract F19628-89-C-0001, and by the United States Army Cecom under contract DAAB07-94-C-H601. Author's address: The MITRE Corporation, Mail Stop A118, 202 Burlington Rd., Bedford, MA 01730-1420 USA.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Braden. Requirements for internet hosts-communication layers. RFC 1122, 1989.
William Clinger. The Scheme 311 compiler: An exercise in denotational semantics. In 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, New York, August 1984. The Association for Computing Machinery, Inc.
D. E. Comer and D. L. Stevens. Internetworking with TCP/IP. Prentice-Hall, 1991–93. Volumes I–III.
William M. Farmer. A partial functions version of Church's simple theory of types. Journal of Symbolic Logic, 55(3):1269–91, 1990. Also MITRE Corporation technical report M88-52, 1988; revised 1990.
William M. Farmer. A simple type theory with partial functions and subtypes. Technical report, The MITRE Corporation, 1991. Submitted to Annals of Pure and Applied Logic.
William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. Little theories. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 567–581. Springer-Verlag, 1992.
William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: an Interactive Mathematical Proof System. Journal of Automated Reasoning, 11(2):213–248, October 1993.
William M. Farmer and F. Javier Thayer. Two computer-supported proofs in metric space topology. Notices of the. American Mathematical Society, 38(9):1133–1138, 1991.
David Gries. The Science of Programming. Springer-Verlag, 1981.
Joshua D. Guttman, John D. Ramsdell, and Mitchell Wand. VLISP: A verified implementation of Scheme. Submitted to Lisp and Symbolic Computation, 1994.
Joshua D. Guttman, Vipin Swarup, and John D. Ramsdell. The VLISP verified Scheme system. Submitted to Lisp and Symbolic Computation, 1994.
C. A. R. Hoare. Notes on data structuring. In O.-J. Dahl, editor, Structured Programming. Academic Press, 1972.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ, 1985.
IEEE Std 1178-1990. IEEE Standard for the Scheme Programming Language. Institute of Electrical and Electronic Engineers, Inc., New York, NY, 1991.
G. Kahn. Natural semantics. In F. J. Bandenburg, G. Vidal-Naquet, and M. Wirsing, editors, Fourth Annual Symbosium on Theoretical Aspects of Computer Science, volume 247 of Lecture Notes in Computer Science, pages 22–39, Berlin, February 1987. Springer-Verlag.
Richard A. Kelsey and Jonathan A. Rees. A tractable Scheme implementation. Submitted to Lisp and Symbolic Computation, 1994.
Keith Loepere. Mach 3 kernel interfaces. Technical report, Open Software Foundation, Cambridge, MA, July 1992. Jointly copyright by Open Software Foundation and Carnegie-Mellon University.
U.S. Department of Defense. Transmission control protocol, military standard. MIL-STD 1778, August 1983.
Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP verified PreScheme compiler. Submitted to Lisp and Symbolic Computation, 1994.
J. Postel. Transmission control protocol. RFC 793, September 1981.
John D. Ramsdell. The revised VLISP PreScheme front end. M 93B095, The MITRE Corporation, August 1993.
D. Sidhu and T. P. Blumer. Some problems with the specification of the military standard transmission control protocol. RFC 964, November 1985.
W. R. Stevens. UNIX Network Programming. Prentice-Hall, Englewood Cliffs, NJ, 1990.
Mitchell Wand. Semantics-directed machine architecture. In Conf. Rec. 9th ACM Symp. on Principles of Prog. Lang., pages 234–241, 1982.
Mitchell Wand and Dino P. Oliva. Proving the correctness of storage representations. In Proceedings of the. 1992 ACM Conference on Lisp and Functional Programming, pages 151–160, New York, 1992. ACM Press.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guttman, J.D., Johnson, D.M. (1994). Three applications of formal methods at MITRE. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_87
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_87
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive