论文部分内容阅读
使用FeaVer对MINIX 3文件系统源代码进行形式化验证，并找到其中的错误代码。在验证的过程中引入测试用具的概念，它的特点是高效性和可复用性。在验证结果的基础上对原来的验证模型进行修改，并建立新的模型。经验证新模型符合应有的正确性属性。以新模型为依据对MINIX 3的源代码进行改进，使操作系统达到一个更可靠的状态。