• DocumentCode
    3345702
  • 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
  • fYear
    1997
  • fDate
    12-14 Nov. 1997
  • Firstpage
    151
  • Lastpage
    160
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on
  • Conference_Location
    Hiroshima, Japan
  • Print_ISBN
    0-8186-8002-4
  • Type

    conf

  • DOI
    10.1109/ICFEM.1997.630422
  • Filename
    630422
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3345702