Title :
The specification-based testing of a trusted kernel: MK++
Author :
Ford, Richard L. ; Simon, Richard T. ; Bevier, William R. ; Smith, Lawrence M.
Author_Institution :
Open Group Res. Inst., Cambridge, MA, USA
Abstract :
The MK++ kernel, a descendant of Mach, was designed and implemented at the Open Group Research Institute. Independently, Computational Logic Inc. 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.
Keywords :
formal specification; operating system kernels; program testing; software reliability; MK++ implementation; MK++ kernel; Mach kernel interface; formal specification; specification based testing; testing strategy; trusted kernel; Atomic layer deposition; Computer bugs; Formal specifications; Kernel; Law; Legal factors; Logic; Performance evaluation; System testing; Yarn;
Conference_Titel :
Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on
Conference_Location :
Hiroshima, Japan
Print_ISBN :
0-8186-8002-4
DOI :
10.1109/ICFEM.1997.630422
