The Community for Technology Leaders
RSS Icon
Subscribe
Hiroshima, JAPAN
Nov. 12, 1997 to Nov. 14, 1997
ISBN: 0-8186-8002-4
pp: 151
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.
ABSTRACT
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.
CITATION
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
19 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool