2007 · 语言与软件

检查每一种可达的可能性

模型检测将系统行为变成可以自动探索的图。

E. 艾伦·爱默生 · 埃德蒙·克拉克 · 约瑟夫·西法基斯

2007图灵奖

视觉指南

奖项，化为图解

阅读图解文字

自动验证成为在硬件和软件中发现隐蔽缺陷的实用工具。

状态空间可能极其庞大；检查模型也不自动保证模型忠实于实际系统。

01 · 核心想法

埃德蒙·克拉克、E. 艾伦·爱默生和约瑟夫·西法基斯发展了模型检测。有限模型描述系统状态及其转换，逻辑性质说明应当满足什么。算法探索模型，并能返回展示要求如何失败的反例。

自动验证成为在硬件和软件中发现隐蔽缺陷的实用工具。

02 · 人物

E. 艾伦·爱默生与埃德蒙·克拉克共同发展模型检测，展示如何自动检查有限状态系统的时态逻辑性质。他强调验证的逻辑基础，以及系统可能的执行过程与所需保证之间的关系。他在得克萨斯大学奥斯汀分校继续研究形式化方法，并与克拉克、约瑟夫·西法基斯共同获奖。

埃德蒙·克拉克推动形式化验证发展为自动模型检测。他与 E. 艾伦·爱默生展示如何检查有限状态系统的时态性质，后来处理实际软硬件中巨大的状态空间。他在卡内基梅隆发展更具扩展性的验证方法和工具，把数学规格与自动寻找错误、获取正确性证据的方法联系起来。

约瑟夫·西法基斯独立开创模型检测，发展验证有限状态系统行为的方法。他在法国把形式模型与分析持续和环境交互的系统的工具联系起来，并推动建立 Verimag 实验室，后来研究嵌入式系统的严格设计。他对共同获奖成果的贡献同时涉及验证理论与可靠反应式系统的实际构造。

03 · 延伸阅读

本站原创讲解依据官方获奖记录。领域标签用于编辑导航。