程序重构提升软件模型检测效率的关键策略

在当前软件模型检测面临处理大型程序困难的情况下，本研究提出了一种创新方法——程序重构预处理，以提升软件模型检测的效率。程序重构的核心思想是将复杂的大型程序分解成一系列保持原始语义一致的小型独立过程。这种方法的优势在于，模型检测算法通常关注过程间的连接关系，即过程总结边。通过预处理，这些边可以在算法执行时分别计算，而非在整个程序上下文中全局搜索，这样显著减少了状态空间的重复探索，从而降低空间和时间复杂度。 程序重构预处理的实施基于程序的线性时序逻辑（Linear Temporal Logic，LTL）公式表达的性质。LTL公式是软件模型的重要组成部分，它们描述了程序的行为约束。作者提出了一个理论框架，明确了程序重构后与原程序语义等价的充分条件，即只要重构后的程序在局部逻辑上与原程序一致，且所有小过程的组合依然符合原系统的整体行为，那么重构后的程序在模型检测中的效果应当相同。 为了验证这一方法的有效性，研究者选取了具体的程序和性质公式，并使用blast（Bounded Model Checking工具）作为实验平台。实验结果显示，经过程序重构预处理后，blast在模型检测方面的性能得到了明显改善，尤其是在大型程序上，时间和空间开销得到了有效控制，这证明了程序重构预处理对于提高软件模型检测效率的实际价值。 程序重构预处理策略不仅解决了软件模型检测处理大型程序的难题，还确保了软件安全性要求得以满足。通过这种方式，开发者可以更有效地评估和改进大型软件系统，降低了模型检测的成本，对于提升软件质量控制和安全性具有重要意义。这项工作为软件开发实践提供了一种实用且高效的工具和技术，有助于推动软件工程领域的发展。