文献类型：期刊文献

中文题名：基于FeaVer的MINIX3验证和改进

英文题名：Verification and Improvement of MINIX 3 Based on FeaVer

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

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

年份：2010

卷号：36

期号：22

起止页码：46

中文期刊名：计算机工程

外文期刊名：Computer Engineering

收录：CSTPCD;;Scopus;北大核心:【北大核心2008】；CSCD:【CSCD2011_2012】；

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

语种：中文

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

外文关键词：formal verification; model check; MINIX 3 operating system; file system

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