Model checking system software with CMC
Model checking system software with CMC
复制标题
带 CMC 的模型检查系统软件
DOI：
10.1145/1133373.1133418
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
D. Engler
中科院分区：
文献类型：
--
作者：
M. Musuvathi;Andy Chou;D. Dill;D. Engler
复杂的系统有错误，涉及在复杂的事件序列中处理不当的角落案例。传统的测试技术通常会忽略这些错误。近年来，像[5]这样的形式验证技术在检查系统的所有可能行为中的属性方面变得流行起来。然而，这些技术涉及生成系统的抽象模型。这样的抽象过程是不可靠的，困难的，并且遗漏了许多实现错误。CMC是一个用于模型检查的框架，它是用C编程语言编写的一大类软件。CMC直接运行软件实现，而不导出代码的抽象模型。我们使用CMC对一个已有的AODV(Ad Hoc On Demand Distance Vector)路由协议的实现进行了建模检查，发现该协议的两个实现[7]、[6]总共存在29个错误。其中之一是AODV协议的实际规范中的错误[3]。我们还在Linux TCP/IPv4堆栈中的IP分段模块上使用了CMC，并验证了其正确性，每个数据包最多可以有4个分段。
Complex systems have errors that involve mishandled corner cases in intricate sequences of events. Conventional testing techniques usually miss these errors. In recent years, formal verification techniques such as [5] have gained popularity in checking a property in all possible behaviors of a system. However, such techniques involve generating an abstract model of the system. Such an abstraction process is unreliable, difficult and miss a lot of implementation errors.CMC is a framework for model checking a broad class of software written in the C programming language. CMC runs the software implementation directly without deriving an abstract model of the code. We used CMC to model check an existing implementation of AODV (Ad Hoc On Demand Distance Vector) routing protocol and found a total of 29 bugs in two implementations [7],[6] of the protocol. One of them is a bug in the actual specification of the AODV protocol [3]. We also used CMC on the IP Fragmentation module in the Linux TCP/IPv4 stack and verified its correctness for up to 4 fragments per packet.