随着代码规模的增大和系统复杂性的增加,软件开发者意识到依靠人工的方式去维护软件系统、排除系统错误已经变得非常困难。形式化方法由于其正确性高、可自动化的特点,已经开始被应用于大型复杂的软件系统中。模型检验作为一种广泛采用的形式化方法,建立在对系统模型的抽象和对性质规约验证的基础之上,利用算法对模型的性质进行验证;模型检验技术不仅适用于系统开发前的安全性和可靠性验证,也适用于系统后期的维护工作。Coccinelle作为基于模型检验技术的代码搜索和转化工具,主要用于解决系统API库接口变化引发的并行演变。它利用描述语言SmPL描述代码模式,还可以在代码中搜索软件错误和漏洞,提升代码质量。SmPL能够理解C程序中的控制逻辑,因此可以精确地在大规模的程序中搜索C语言的代码块。目前SmPL支持条件语句、循环语句等不同控制结构的模式描述,但是缺少了对do-while循环结构的支持,这会限制SmPL的表达能力,影响程序匹配的准确性。本文针对Coccinelle中缺少的do-while循环结构进行了建模和公式设计。我们通过对C语言代码中的do-while循环结构进行建模,抽象为具有通用性的控制流图。在SmPL中,需要将do-while循环的控制结构转为CTL公式;通过对do-while的语法定义的补充,完成从代码到AST,再到CTL公式的转换过程,从而拓展SmPL的表意能力,完善了Coccinelle的控制流功能。本文的成果主要包括:1.我们对拓展后的Coccinelle进行了测试,包含了功能测试和性能测试,测试结果显示拓展后的Coccinelle可以正确地解析包含复合控制结构和嵌套结构下的do-while循环。2.我们利用拓展后的Coccinelle对Linux内核中的代码模式进行了调研,统计了Linux内核中do-while结构的数量和代码分布情况。还成功地对现实中一个具体的内核问题进行了验证,结果说明本文成果兼具正确性和实用性。