逻辑模型检查
我们用于检查软件设计正确性的方法在大多数工程学科上都是标准的。该方法称为模型检查。当软件本身无法彻底验证时，我们可以构建一个简化的底层设计模型，该模型保留了其基本特征，但避免了已知的复杂性来源。当整体规模的验证不可实施时，设计的模型通常是可以被验证的。
当遇到复杂的设计问题时，桥梁制造商和飞机设计师应用了大致相同的技术。通过构建和分析模型（或原型），可以降低实施包含细微缺陷设计的风险。 一旦达到实施阶段，定位或修复设计错误通常太昂贵。复杂软件的设计也是如此。
我们在本书中讨论的建模技术特别适用于并发软件，而幸运的是，它也是最难以使用传统方法进行调试和测试的。
我们将构建的模型可以看作是小程序，最初写入的看起来像是一种奇怪的抽象语言。用这种语言编写的模型实际上是可执行的。他们指定的行为可以通过模型检查器在寻找逻辑错误时进行详尽的模拟和探索。构建和执行这些高级模型可能既有趣又富有洞察力。即使在执行任何精确检查之前，它通常也会对可能带来新解决方案的编程问题提供足够不同的视角。
逻辑模型检查器旨在使用有效的过程来表征所有可能的执行，而不是一个小的子集，就像在试验执行中看到的那样。由于它可以探索所有行为，因此模型检查器可以对设计模型应用一系列完整的检查，并且可以成功识别不可执行的代码，或者并发执行时可能发生的死锁。它甚至可以检查是否符合复杂的用户定义的正确性标准。模型检查器在系统设计中定位细微错误的能力是无与伦比的，比基于人工检查，测试或随机模拟的更传统方法提供了更大的控制。
模型检查技术已应用于大规模工业应用程序中，以减少对测试的依赖、在设计周期的早期检测设计缺陷、在最终设计中证明它们的缺失。 本书讨论了这些应用程序的一些示例。
