软件模型检测

模型检测通过穷尽探索系统模型的可达状态，自动验证其是否满足时序逻辑规范。

Definition

模型检测是一种自动验证技术，给定一个系统的有限状态模型和时序逻辑规范，它会穷尽检查该规范是否成立，如果规范不成立，则会生成一个反例追踪。

Scope

本主题涵盖了针对时序逻辑属性（安全性与活性）的有限状态和并发系统的自动验证、状态爆炸问题及其应对技术（使用二元决策图的符号表示、偏序约简、抽象）、基于SAT/SMT的有界模型检测，以及软件的反例引导抽象细化。

Core questions

• 如何通过探索所有可达状态来验证属性？
• 什么是状态爆炸问题，以及如何缓解？
• 符号方法和有界方法如何扩展模型检测的规模？
• 无限状态软件系统如何抽象为有限模型？

Key theories

时序逻辑模型检测

克拉克（Clarke）、埃默森（Emerson）和西斯特拉（Sistla），以及独立研究的凯勒（Queille）和西法基斯（Sifakis），引入了自动检查有限状态并发系统是否符合时序逻辑规范的算法。

符号模型检测

伯奇（Burch）及其同事使用二元决策图符号化地表示状态集，从而能够验证具有天文数字般状态的系统，并克服了朴素的状态爆炸问题。

Clinical relevance

模型检测用于验证硬件设计、通信协议以及并发和安全关键型软件，它能发现测试遗漏的细微错误，并提供指出故障的反例。其自动化特性使其有别于交互式定理证明。

History

在普努埃利（Pnueli）引入程序时序逻辑的基础上，克拉克（Clarke）和埃默森（Emerson）以及独立研究的凯勒（Queille）和西法基斯（Sifakis）在大约1981-82年间提出了模型检测，这项工作后来获得了图灵奖的认可。20世纪90年代，采用二元决策图的符号模型检测和基于SAT的有界模型检测极大地扩展了其应用范围，而抽象细化方法则将其引入了软件领域。

Debates

应对状态爆炸

核心挑战是状态数量随系统规模呈指数级增长；研究人员讨论了符号表示、抽象、偏序约简和有界检测的最佳组合，以保持验证的可行性。

Key figures

• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis
• Kenneth McMillan
• Amir Pnueli

Seminal works

• clarke1986
• queille1982
• burch1992

Frequently asked questions

模型检测与定理证明有何不同？

模型检测是全自动的，对有限或抽象模型穷尽探索系统的状态空间，而定理证明则使用逻辑推导（通常是交互式的），可以处理无限状态系统，但需要更多的人工指导。

什么是状态爆炸问题？

它是指随着系统组件或变量的增加，可达状态数量呈指数级增长，这限制了朴素模型检测的应用，并促使了符号、有界和基于抽象的技术的发展。