期刊名称：International Journal of Wireless and Microwave Technologies(IJWMT)
印刷版ISSN：2076-1449
电子版ISSN：2076-9539
出版年度：2011
卷号：1
期号：3
页码：62-69
出版社：MECS Publisher
摘要：There is increasing pressure on providing a high degree of assurance of operation system’s security and functionality. Formal verification is the only known way to guarantee that a system is free of programming errors. We study on formal verification of operation system kernel in system implementation level and take theorem proving and model checking as the main technical methods to resolve the key techniques of verifying operation system kernel in C implementation level. We present a case study to the verification of real-world C systems code derived from an implementation of μC/OS – II in the end.
关键词：OS kernel; formal verification; theorem proving; model checking
