Formal Engineering Methods, International Conference on (1997)
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.
L. M. Smith, R. T. Simon, W. R. Bevier and R. L. Ford, "The Specification-Based Testing of a Trusted Kernel: MK++," Formal Engineering Methods, International Conference on(ICFEM), Hiroshima, JAPAN, 1997, pp. 151.