图灵奖得主Joseph Sifakis：将模型检测从学术应用至产业界的功臣 | CCF-GAIR 2018

软件工程专业的同学想必都很熟悉下面这起惨剧：1996 年 6 月 4 日，由欧洲 12 国联合研制的阿丽亚娜 (Ariane) 5 型运载火箭，在首次发射后因为一行代码的溢出错误导致火箭升空约 37 秒时爆炸，造价几亿欧元的火箭就这样悲剧收场。

如此重大的发射任务事前势必经过了周密的检查，但为什么还是没能避免惨剧的发生？举个例子大家就懂了，这就好比箭已离弦，导弹飞机离地升空，根本不可能在空中进行重启操作。再加上如火箭、飞机这样的军工，航天领域应用的软件代码越来越复杂，一旦发生代码溢出和死循环，后果也将越发不可承受。同样的悲剧也绝非孤例，微软的 Windows Azure 因受到一个闰日缺陷而宕机长达 30 多小时；亚马逊平台故障导致 0.07% 的用户数据最终无法复原。

在这样的背景下，学术界和工业界开始要求在常规测试之外采用更加严格的检测手段来避免悲剧。这个额外的检测手段就是形式化证明，但当时形式化证明中的半自动定理证明工具仍需要人力参与，由此造成的效率不高导致无法大范围应用，于是在一些科学家的努力下，一个更具效率的、无需人类参与的自动化证明成果诞生了。

它就是模型检测（Model Checking），这项成果是由 Verimag 实验室创始人 Joseph Sifakis 与 CMU 教授 Clarke 和得克萨斯大学奥斯汀分校教授 Emerson 于 1981 年分别独立提出的。其中，Sifakis 与 Thomas A. Henzinger、Sergio Yovine 将模型检查方法成功应用于实时系统的验证。三位科学家也于 2008 年 2 月 4 日因「在将模型检查发展为被硬件和软件业中所广泛采纳的高效验证技术上的贡献」获得 2007 年的图灵奖。

由中国计算机学会（CCF）主办，雷锋网(公众号：雷锋网)与香港中文大学（深圳）承办的 CCF-GAIR 2018 大会计划于 6 月 29 日至 7 月 1 日在深圳举行。在第一天的人工智能主论坛上，2007 年图灵奖得主，欧洲科学院院士、法国科学院院士、美国文理科学院院士、美国国家工程院院士 Joseph Sifakis 将作为重磅嘉宾莅临现场并带来主题演讲。

Joseph Sifakis 出生于希腊，1960 年代求学于希腊的雅典国立科技大学的电子工程系，随后他便在 1970 年代前往法国的 University of Grenoble 计算机系学习攻读了硕士学位和工程师博士学位，并在 1972 年—1979 年期间留校指导论文和任教。

Joseph Sifakis 虽然生于希腊，但他的研究成就大多是在法国完成的，Joseph Sifakis 还因为突出的学术成就在 2001 年被法国国家科研中心授予银质奖章，目前 Joseph Sifakis 在法国嵌入式系统研究中心 Verimag 实验室担任 Senior CNRS Researcher，同时他还是 Verimag 实验室的创始人。

1993 年，Joseph Sifakis 联合 CNRS 和 Grenoble 大学创办了位于法国的学术研究实验室 Verimag 实验室，该实验室主攻嵌入式系统理论和技术研究，在过去的 15 年时间里，Verimag 实验室在嵌入式系统的同步语言、验证、测试和建模等前沿技术的发展方面做出了积极贡献。Verimag 实验室开发的工具已经落地为商业 CASE 工具, 并被在产业应用中得到广泛使用。

另外，在 Joseph Sifakis 的个人主页，也介绍了其当前主攻严密系统设计（Rigorous System Design），Component-based Construction - BIP 和图灵奖成果—模型检测（Model Checking）这三个研究领域。

严密系统设计（Rigorous System Design）

Joseph Sifakis 团队研究混合硬/软件系统设计，该系统设计可作为一个涉及指导将需求达到可保证正确实现的步骤的正式迭代过程。Joseph Sifakis 团队要求该混合硬/软件系统设计是基于模型，基于组件以及可负责。该先进的设计方法由 BIP（Behavior，Interaction，Priority）理论和工具支撑。

Component-based Construction – BIP

Joseph Sifakis 团队研究理论，方法以及工具来打造由异构部件（heterogeneous component）组成的系统。该研究主要聚焦以下三项挑战：

在产业界取得瞩目成功的图灵奖成果，模型检测（Model Checking）

下面来具体介绍下这一已被广泛应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中的自动验证技术。

介绍模型检测要从开篇提到的形式化证明提起，因为模型检测是形式化证明中的自动化证明手段。形式化证明中的形式化简单来说就是将检测要做的具体事项用无二义性的数学语言描述，证明即基于已知条件，再依据定理推导出结论，这也就是计算机领域的公理系统。基于这套公理系统，程序员们就可借助函数命令这种软件形式化证明——定理证明来实现在军工和航空等领域的检测，但是这种类似的半自动定理证明工具依旧需要人的参与。

那么证明手段自动化能否实现？这就引出了图灵奖获奖成果——模型检测。

模型检测不同于步步按照公理系统进行证明和推论的定理证明，它依赖的是对程序行为空间的穷尽搜索，也就是自动化遍历。另外，我们还需验证模型是否满足给定的形式化规约（Formal Specification）。同时对程序行为空间的穷尽搜索的自动化遍历相当吃计算机内存，为了解决该问题，后来的科学家们提出了包括符号模型检验（Symbolic Model Checking），偏序约减（Partial Oder Reduction）以及状态抽象（Abstraction）等压缩状态表达和缩减验证空间的优化技术。模型检验也终于从学术界应用到如芯片检测、通信协议、外部设备主控软件、嵌入式系统（如在飞机、火车、火箭、卫星或移动电话）以及安全算法等工业检测领域。

雷锋网 AI 科技评论发现，上面提及的嵌入式系统「碰巧」是 Joseph Sifakis 于 1993 年创办的 Verimag 实验室的主攻研究。自 1998 年起，Sifakis 就积极推动嵌入式系统面世并为该领域的国际和现场研究社区的组建作出了贡献。他一直担任 ARTIST 欧洲嵌入式系统设计卓越网络的科学家协调员（Scientific Coordinator），帮助协调欧洲领先的嵌入式系统团队。Sifakis 积极协助在欧洲成立 ARTEMISIA 嵌入式系统工业协会，同时他还是 EmSoft 会议和嵌入式系统周的联合创始人。

近几年，随着计算机整体技术水平的发展，被公认为与人工智能，AR/VR 并列未来三大主流技术的物联网，即信息物理融合系统（Cyber－Physical System），物联网系统（Internet of Things）的重要地位愈发凸显，而将模型检测推向应用的 Joseph Sifakis 不止用该自动验证技术保证了航空，军工等安全攸关行业的安全落地发展，还对物联网的基础支撑技术：嵌入式系统深有研究，未来随着物联网应用的进一步落地，我们也将面临更加复杂的传感器，通信等技术，这也将对更加复杂和开放嵌入式系统进行验证带来的新挑战，届时如何避免悲剧，保证系统安全就显得至关重要。

雷锋网 AI 科技评论了解到，Joseph Sifakis 在去年 9 月的第五届 HLF（图灵奖获得者演讲大会）上发表了针对 IoT 未来的演讲。Joseph Sifakis 如此看待 IoT 的未来：

IoT 革命的背后是，对互联的智能对象提供的资源管理自动化和增强人们生活质量需求的日益增长。IoT 愿景里有智能电网、智能交通系统、智能卫生保健服务、自动化银行服务、智能工厂等等，其中智能化互联对象之间的协调就显得至关重要。要实现该 IoT 愿景，我们有着长期内需跨越的技术障碍，同时也要认识到现阶段的基础设施网络并不安全也不保险，这就需要发展混合关键性系统的设计流程。

看到这里，想必你也跟 AI 科技评论达成了共识：从模型检测到嵌入式设备，再到物联网时代，Joseph Sifakis 最有话语权。

第三届 CCF-GAIR 全球人工智能与机器人峰会将于 6 月 29 日-7 月 1 日席卷鹏城，届时将会有 1 个主会场和 11 个专场（仿生机器人专场，机器人行业应用专场，CV 专场，智能安全专场，金融科技专场，自动驾驶专场，NLP 专场，AI+ 专场，AI 芯片专场，IoT 专场，投资人专场），意欲从产学研多个维度，呈现出更富前瞻性与落地性的会议内容。

而 Joseph Sifakis 也将作为重磅嘉宾莅临现场并带来主题演讲，所以你确定不来当场了解一下图灵奖得主 Joseph Sifakis 的最新研究与思考吗？目前四折门票正在火热销售中，限量 100 张，详情可访问大会官网了解。

原文发布时间为：2018-05-21

本文作者：刘鹏

本文来自云栖社区合作伙伴“雷锋网”，了解相关信息可以关注“雷锋网”。