C程序错误定位：模型检查器与自动化方法

"这篇论文探讨了使用模型检查器在C程序中自动定位错误的方法，重点关注在给定反例的情况下，如何有效地找出导致错误行为的代码片段。作者们使用了一个仪表化的有界模型检查器CBMC，通过对程序进行扩展并引入异常谓词来隔离可能的故障组件。他们通过否定原始规范并再次进行模型检查来验证新系统，从而确定需要修正的组件和相应的修复策略。这项研究得到了欧盟的支持，并强调了在复杂软件系统中，自动故障定位工具的重要性。" 在软件开发过程中，调试是不可或缺的一环，尤其是随着系统复杂性的增加，对高效调试工具的需求也日益增长。该论文的焦点在于故障定位，即在检测到程序存在错误（通过反例展示）后，如何准确地找到问题源头。反例是模型检查器在验证程序不符合规范时提供的一个证明错误行为的运行实例。 作者们提出的自动错误定位方法基于C语言程序和一个给定的规范。如果程序违反了规范，模型检查器将提供一个反例。利用这个反例，他们固定程序的输入，然后为每个程序组件引入异常谓词。如果异常谓词为真，表示该组件可能存在问题。通过悬挂这些组件的原始行为并用新的输入替换，目标是找出需要调整以满足原始规范的异常谓词及其对应组件。 为实现这一目标，他们首先否定原始规范，这样如果无法满足新规范，就表明某些组件需要改变。接着，他们再次运行模型检查器来验证这个新系统。如果模型检查器发现失败的运行，这将揭示哪些异常谓词对应的组件工作异常，从而指导错误修复。 这项工作的独特之处在于其自动化程度，通过模型检查和异常谓词的使用，能够减少手动调试的复杂性和时间消耗。论文的实验结果证明了这种方法的有效性，为C程序的自动故障定位提供了有力工具。在当前的软件工程实践中，这样的方法对于提高开发效率和减少错误修复的难度具有重要意义。