图灵奖得主Joseph Sifakis：将模型检测从学术应用至

　　原标题：图灵奖得主Joseph Sifakis：将模型检测从学术应用至产业界的功臣 CCF-GA

　　软件工程专业的同学想必都很熟悉下面这起惨剧：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 年期间留校指导论文和任教。

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

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

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

　　一个异构部件（heterogeneous component）中增量组成的框架。异质性的三个不同来源被认为与交互、执行和抽象相关联

　　通过构建基本系统属性的 Correctness-by-construction，例如互斥，无死锁和进度来最小化后验验证

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

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

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