论文部分内容阅读
如何保证软件系统的正确性一直是人们所关注的问题，为了能够准确、快速地找到软件系统中存在的问题，研究者们研发出了对软件系统进行形式化验证的工具。在本文中，我们将使用FeaVer对MINIX3操作系统中文件系统的源代码进行形式化验证。在验证的过程中我们引入了测试用具的概念，它的特点是高效性和可复用性。首先我们根具和对应的源文件交由FeaVer来验证，FeaVer会根据测试用具的内容自动从源代码中提取验证模型并进行验证。我们证明了MINIX3文件系统中绝大部分的源代码都是正确的，但同时我们也证明了在其文件系统的源代码中也确实存在错误，并找到了出错的代码。于是我们在验证结果的基础上对原来的验证模型进行了修改，并且建立了新的模型。经验证新模型符合我们所定义的正确性属性。最后我们以新模型为依据对MINIX3的源代码进行了改进，使操作系统达到了一个更可靠的状态。