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

　　模型检测不同于步步按照公理系统进行证明和推论的定理证明，它依赖的是对程序行为空间的穷尽搜索，也就是自动化遍历。另外，我们还需验证模型是否满足给定的形式化规约（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 不止用该自动验证技术保证了航空，军工等安全攸关行业的安全落地发展，还对物联网的基础支撑技术：嵌入式系统深有研究，未来随着物联网应用的进一步落地，我们也将面临更加复杂的传感器，通信等技术，这也将对更加复杂和开放嵌入式系统进行验证带来的新挑战，届时如何避免悲剧，保证系统安全就显得至关重要。

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

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

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

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