Formal Engineering Methods, International Conference on (1997)
Nov. 12, 1997 to Nov. 14, 1997
Lawrence M. Smith , Computational Logic, Inc.
Richard T. Simon , The Open Group Research Institute
William R. Bevier , Computational Logic, Inc.
Richard L. Ford , The Open Group Research Institute
The MK++ kernel, a descendant of Mach, was designed and implemented at the Open Group Research Institute. Independently, Computational Logic had developed a formal specification for the Mach kernel interface. We report on the adaptation of this specification to MK++, and its use in the derivation of a testing strategy for the MK++ implementation. The results and utility of the tests are discussed.
Lawrence M. Smith, Richard T. Simon, William R. Bevier, Richard L. Ford, "The Specification-Based Testing of a Trusted Kernel: MK++", Formal Engineering Methods, International Conference on, vol. 00, no. , pp. 151, 1997, doi:10.1109/ICFEM.1997.630422