基于FeaVer的MINIX3验证和改进  

Verification and Improvement of MINIX 3 Based on FeaVer

作　　者：全嘉辉[1] 张欢欢[1] 

机构地区：[1]华东理工大学信息科学与工程学院

出　　处：《计算机工程》2010年第22期46-48,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(60703026);广东省教育部产学研合作基金资助项目(2007A090601001)

摘　　要：使用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.

关 键 词：形式化验证 模型检测 MINIX 3操作系统 文件系统 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]