10.5.5  什么是模型检测

尽管关于模型检测的讨论超出了本书的范围，但是我们在这里对它做一下介绍，这样一旦您准备好了处理大且复杂的并行程序或大规模多线程应用程序，您能够对使用的工具有一些认识。本书给出了对于多核和多线程编程(www.cppentry.com)的一些更具挑战性的问题。但本书仅仅做了简要介绍。我们介绍了向着并行化的逻辑模型发展的声明式并行编程(www.cppentry.com)技术。逻辑模型将最终帮助开发者应对大规模并行多核计算机。模型检测技术可用来自动化具有声明式架构的多线程或并行程序的检测。模型检测是用来验证有限状态并发系统的技术[Huth，Ryan，2004]。模型检测用来判断给出的模型是否是期望的模型。在本章中作为例子的PBS方法，给出了应用程序的逻辑模型，该模型可以被形式化并用于模型检测工具。您可能对了解Kripke架构被用于可能世界和模型检测的形式化表示感兴趣[Meyer，Van der Hoek，2004]。