先说点题外话。经过长时间的感受之后，认为读文献还是用纸的好，目前打印了一批，是准备在本科期间精读完的。方便做标记，也方便找。而且不用盯着屏幕看，很舒服。

测试分布式系统的bug往往需要非常错综复杂的执行序列，一个系统运行几小时、几天、几周。。才有可能触发代码中的问题。

检查 Bug 的方法，一是 Model Checking。它能够接受一个由实际代码简化来的系统，然后穷举系统执行的所有可能性。但是在现实中有很多缺点：建模非常困难。写模型比写代码化的时间多多了。并且检查这个抽象的模型，还是容易忽略掉实际代码实现里面的问题。

文章的贡献：

一是提出了一个新的 Model Checker，CMC，它能够直接对 C 和 C++ 代码实现进行检查，避免了抽象过程中的错误丢失，并且不用花时间去建模了。额外的好处是代码一经改动可以立即检查。

二是说明了 CMC 在实际的系统中能够得到较好的应用。通过对三个版本的 AODV 网络协议的模型检查，可以预见 CMC 能够应用于其他的系统，尤其是其他的网络协议。

复杂的系统有复杂的问题。现实中的系统有很多由错综复杂的执行顺序触发的边界情况没有在代码中得到处理。他们在系统中就像是“残渣”一样，日积月累，最后使整个系统瘫痪。我们发现了这种错误之后，通常就很难诊断问题的原因了。因为这些问题并不可复现。导致这些问题的执行流实在是太长，没有办法去重建在车祸现场之前到底发生了什么。

形式化验证是针对这种深层次的问题的一个可能的办法。它能够系统地列举系统的所有的可能状态。一个基本的模型检测从系统的一个初始状态开始，并且通过非确定地执行事件递归地生成后继的系统状态。所有的状态都被储存在一个哈希表里来确保每一个状态都至多被遍历到一次。这个过程一直持续到所有的状态都能够遍历完成，或者是所有的系统资源都耗尽。这种状态图探索的办法相较于不切实际的大量测试，能够在达到其效果地同时，避免测试当中的冗余。

传统的模型检测经常假设系统设计是以一种很高的层次，抽象掉实际实现的很多细节的。验证实际上的代码就需要从代码重建这些抽象的描述。这个过程需要大量的人工，妨碍到了模型检测在实际系统当中的应用。并且，人在手工抽象过程中的失误也会导致假阳性或漏报。这种错误既可能在构建模型的时候发生，也有可能在系统演进的过程中发生。

。。。

对实际实现进行模型检测的这个想法已经在几个工具当中被采用了。Verisoft，系统地执行 C 实现代码但是不记录状态。其他的软件模型检测工具比如说 [3][25] 是专门用于 Java 程序中的特定 Class 的。CMC 采用了多个研究当中的技术来设计，把它用于 C 和 C++ 编写的程序，它们是工业界应用到的主要语言。

我们的终极目标是检查所有的代码；但一开始我们关注网络代码。这种代码天然地遵从一种“事件驱动”的编程模型，能够很好地与模型检查工具相契合。网络代码的正确新很重要，因为它们常常处于服务的中心，并且经常是容易受攻击的对象。但是网络协议又难以设计、实现和测试因为网络中包括多台机器之间的复杂行为，并且需要处理多种网络错误，如丢包、连接失败，这些在测试环境中是很难控制的。模型检测就很擅长检查这些相互作用。

。。。