摘要
使用FeaVer对MINIX3文件系统源代码进行形式化验证,并找到其中的错误代码。在验证的过程中引入测试用具的概念,它的特点是高效性和可复用性。在验证结果的基础上对原来的验证模型进行修改,并建立新的模型。经验证新模型符合应有的正确性属性。以新模型为依据对MINIX3的源代码进行改进,使操作系统达到一个更可靠的状态。
FeaVer is used to perform a formal verification of source codes of MINIX 3 file system, and the error codes are found. In the procedure of verification, the concept of test harness is introduced, whose characteristics are efficient and reproducible. The original model based on the verification results is modified and a new model is built. It is verified that the new model conforms to the correctness property specified. The source files of MINIX 3 are upgraded according to the new model to make the operating system more reliable.
出处
《计算机工程》
CAS
CSCD
北大核心
2010年第22期46-48,共3页
Computer Engineering
基金
国家自然科学基金资助项目(60703026)
广东省教育部产学研合作基金资助项目(2007A090601001)
