Model Checking

模型检验(model checking)是用于验证软件和硬件的正确性的一种方法。所谓正确性，就是软件或硬件是否正确实现了我们所希望它所具有的功能。

验证正确性的方法有很多。例如，当我们想要验证一段程序的正确性时，可以把代码发给同伴让他看看写的有没有问题（这个过程不需要对代码做任何执行，称为静态分析(static analysis)）；也可以造一些样例测试模型的输出是否正确，这称为测试(testing)。静态分析和测试可以用来发现代码中的错误，而无法保证除此之外没有别的错误了。模型检验希望能够对“待验证的”软件和硬件建立一个完全对应的数学模型，然后验证该数学模型在所有“状态”下都符合我们的功能要求。这样就把验证正确性分为了两步，一部分是待验证的软硬件是否和数学模型相对应，这部分验证称为validation test；第二部分也就是我们将更着重讨论的部分，就是验证该数学模型的正确性。这一过程最强有力的保证是用形式化方法检验数学模型的正确性，称为形式化验证(formal verification)。