Abstract:
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.
Key words:
formal verification,
model check,
MINIX 3 operating system,
file system
摘要： 使用FeaVer对MINIX 3文件系统源代码进行形式化验证，并找到其中的错误代码。在验证的过程中引入测试用具的概念，它的特点是高效性和可复用性。在验证结果的基础上对原来的验证模型进行修改，并建立新的模型。经验证新模型符合应有的正确性属性。以新模型为依据对MINIX 3的源代码进行改进，使操作系统达到一个更可靠的状态。
关键词:
形式化验证,
模型检测,
MINIX 3操作系统,
文件系统
CLC Number:
QUAN Jia-Hui, ZHANG Huan-Huan. Verification and Improvement of MINIX 3 Based on FeaVer[J]. Computer Engineering, 2010, 36(22): 46-48.
全嘉辉, 张欢欢. 基于FeaVer的MINIX 3验证和改进[J]. 计算机工程, 2010, 36(22): 46-48.