Model Checking

释义 Definition

模型检测：一种形式化验证方法，把系统（如软件/硬件/协议）抽象成“模型”，再用自动化算法检查该模型是否满足给定的性质（常见如安全性、活性、时序逻辑性质）。也常译为“模型检验”。（在其他语境中亦可指对“模型”进行检查/核对，但最常见含义是形式化验证。）

发音 Pronunciation (IPA)

/ˈmɑːdəl ˈtʃekɪŋ/

例句 Examples

We used model checking to verify the traffic-light controller.
我们用模型检测来验证交通灯控制器。

Model checking can automatically find subtle concurrency bugs that are hard to reproduce in testing.
模型检测可以自动发现那些在测试中很难复现的细微并发缺陷。

词源 Etymology

由 model（模型） + checking（检查/检验） 组合而成。“模型检测”作为计算机科学中的术语在20世纪后期随形式化方法发展而普及，强调“用可计算的方式对系统模型进行性质检验”。

相关词 Related Words

• Verification
• Formal Methods
• Temporal Logic
• Model
• Specification
• State Space
• Safety
• Liveness
• Automata

文学与著作中的用例 Literary Works

• Edmund M. Clarke, Orna Grumberg, Doron A. Peled：《Model Checking》（书名即包含该词组）
• Christel Baier, Joost-Pieter Katoen：《Principles of Model Checking》
• Gerard J. Holzmann：《The SPIN Model Checker: Primer and Reference Manual》（讨论与使用“model checking”方法的经典著作）