Nov. 12, 1997 to Nov. 14, 1997
Richard L. Ford , The Open Group Research Institute
Richard T. Simon , The Open Group Research Institute
William R. Bevier , Computational Logic, Inc.
Lawrence M. Smith , Computational Logic, Inc.
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.
Richard L. Ford, Richard T. Simon, William R. Bevier, Lawrence M. Smith, "The Specification-Based Testing of a Trusted Kernel: MK++", ICFEM, 1997, Formal Engineering Methods, International Conference on, Formal Engineering Methods, International Conference on 1997, pp. 151, doi:10.1109/ICFEM.1997.630422