圖靈獎得主Joseph Sifakis：將模型檢測從學(xué)術(shù)應(yīng)用至產(chǎn)業(yè)界的功臣 | CCF-GAIR 2018

軟件工程專業(yè)的同學(xué)想必都很熟悉下面這起慘劇：1996 年 6 月 4 日，由歐洲 12 國聯(lián)合研制的阿麗亞娜 (Ariane) 5 型運載火箭，在首次發(fā)射后因為一行代碼的溢出錯誤導(dǎo)致火箭升空約 37 秒時爆炸，造價幾億歐元的火箭就這樣悲劇收場。

如此重大的發(fā)射任務(wù)事前勢必經(jīng)過了周密的檢查，但為什么還是沒能避免慘劇的發(fā)生？舉個例子大家就懂了，這就好比箭已離弦，導(dǎo)彈飛機離地升空，根本不可能在空中進行重啟操作。再加上如火箭、飛機這樣的軍工，航天領(lǐng)域應(yīng)用的軟件代碼越來越復(fù)雜，一旦發(fā)生代碼溢出和死循環(huán)，后果也將越發(fā)不可承受。同樣的悲劇也絕非孤例，微軟的 Windows Azure 因受到一個閏日缺陷而宕機長達 30 多小時；亞馬遜平臺故障導(dǎo)致 0.07% 的用戶數(shù)據(jù)最終無法復(fù)原。

在這樣的背景下，學(xué)術(shù)界和工業(yè)界開始要求在常規(guī)測試之外采用更加嚴格的檢測手段來避免悲劇。這個額外的檢測手段就是形式化證明，但當時形式化證明中的半自動定理證明工具仍需要人力參與，由此造成的效率不高導(dǎo)致無法大范圍應(yīng)用，于是在一些科學(xué)家的努力下，一個更具效率的、無需人類參與的自動化證明成果誕生了。

它就是模型檢測（Model Checking），這項成果是由 Verimag 實驗室創(chuàng)始人 Joseph Sifakis 與 CMU 教授 Clarke 和得克薩斯大學(xué)奧斯汀分校教授 Emerson 于 1981 年分別獨立提出的。其中，Sifakis 與 Thomas A. Henzinger、Sergio Yovine 將模型檢查方法成功應(yīng)用于實時系統(tǒng)的驗證。三位科學(xué)家也于 2008 年 2 月 4 日因「在將模型檢查發(fā)展為被硬件和軟件業(yè)中所廣泛采納的高效驗證技術(shù)上的貢獻」獲得 2007 年的圖靈獎。

由中國計算機學(xué)會（CCF）主辦，雷鋒網(wǎng)與香港中文大學(xué)（深圳）承辦的 CCF-GAIR 2018 大會計劃于 6 月 29 日至 7 月 1 日在深圳舉行。在第一天的人工智能主論壇上，2007 年圖靈獎得主，歐洲科學(xué)院院士、法國科學(xué)院院士、美國文理科學(xué)院院士、美國國家工程院院士 Joseph Sifakis 將作為重磅嘉賓蒞臨現(xiàn)場并帶來主題演講。

Joseph Sifakis 出生于希臘，1960 年代求學(xué)于希臘的雅典國立科技大學(xué)的電子工程系，隨后他便在 1970 年代前往法國的 University of Grenoble 計算機系學(xué)習(xí)攻讀了碩士學(xué)位和工程師博士學(xué)位，并在 1972 年—1979 年期間留校指導(dǎo)論文和任教。

Joseph Sifakis 雖然生于希臘，但他的研究成就大多是在法國完成的，Joseph Sifakis 還因為突出的學(xué)術(shù)成就在 2001 年被法國國家科研中心授予銀質(zhì)獎?wù)拢壳?Joseph Sifakis 在法國嵌入式系統(tǒng)研究中心 Verimag 實驗室擔任 Senior CNRS Researcher，同時他還是 Verimag 實驗室的創(chuàng)始人。

1993 年，Joseph Sifakis 聯(lián)合 CNRS 和 Grenoble 大學(xué)創(chuàng)辦了位于法國的學(xué)術(shù)研究實驗室 Verimag 實驗室，該實驗室主攻嵌入式系統(tǒng)理論和技術(shù)研究，在過去的 15 年時間里，Verimag 實驗室在嵌入式系統(tǒng)的同步語言、驗證、測試和建模等前沿技術(shù)的發(fā)展方面做出了積極貢獻。Verimag 實驗室開發(fā)的工具已經(jīng)落地為商業(yè) CASE 工具, 并被在產(chǎn)業(yè)應(yīng)用中得到廣泛使用。

另外，在 Joseph Sifakis 的個人主頁，也介紹了其當前主攻嚴密系統(tǒng)設(shè)計（Rigorous System Design），Component-based Construction - BIP 和圖靈獎成果—模型檢測（Model Checking）這三個研究領(lǐng)域。

嚴密系統(tǒng)設(shè)計（Rigorous System Design）

Joseph Sifakis 團隊研究混合硬/軟件系統(tǒng)設(shè)計，該系統(tǒng)設(shè)計可作為一個涉及指導(dǎo)將需求達到可保證正確實現(xiàn)的步驟的正式迭代過程。Joseph Sifakis 團隊要求該混合硬/軟件系統(tǒng)設(shè)計是基于模型，基于組件以及可負責。該先進的設(shè)計方法由 BIP（Behavior，Interaction，Priority）理論和工具支撐。

Component-based Construction – BIP

Joseph Sifakis 團隊研究理論，方法以及工具來打造由異構(gòu)部件（heterogeneous component）組成的系統(tǒng)。該研究主要聚焦以下三項挑戰(zhàn)：

• 一個異構(gòu)部件（heterogeneous component）中增量組成的框架。異質(zhì)性的三個不同來源被認為與交互、執(zhí)行和抽象相關(guān)聯(lián)

• 通過構(gòu)建基本系統(tǒng)屬性的 Correctness-by-construction，例如互斥，無死鎖和進度來最小化后驗驗證

• 為組件集成和滿足給定要求的粘合代碼提供自動支持

在產(chǎn)業(yè)界取得矚目成功的圖靈獎成果，模型檢測（Model Checking）

下面來具體介紹下這一已被廣泛應(yīng)用于計算機硬件、通信協(xié)議、控制系統(tǒng)、安全認證協(xié)議等方面的分析與驗證中的自動驗證技術(shù)。

介紹模型檢測要從開篇提到的形式化證明提起，因為模型檢測是形式化證明中的自動化證明手段。形式化證明中的形式化簡單來說就是將檢測要做的具體事項用無二義性的數(shù)學(xué)語言描述，證明即基于已知條件，再依據(jù)定理推導(dǎo)出結(jié)論，這也就是計算機領(lǐng)域的公理系統(tǒng)。基于這套公理系統(tǒng)，程序員們就可借助函數(shù)命令這種軟件形式化證明——定理證明來實現(xiàn)在軍工和航空等領(lǐng)域的檢測，但是這種類似的半自動定理證明工具依舊需要人的參與。

那么證明手段自動化能否實現(xiàn)？這就引出了圖靈獎獲獎成果——模型檢測。

模型檢測不同于步步按照公理系統(tǒng)進行證明和推論的定理證明，它依賴的是對程序行為空間的窮盡搜索，也就是自動化遍歷。另外，我們還需驗證模型是否滿足給定的形式化規(guī)約（Formal Specification）。同時對程序行為空間的窮盡搜索的自動化遍歷相當吃計算機內(nèi)存，為了解決該問題，后來的科學(xué)家們提出了包括符號模型檢驗（Symbolic Model Checking），偏序約減（Partial Oder Reduction）以及狀態(tài)抽象（Abstraction）等壓縮狀態(tài)表達和縮減驗證空間的優(yōu)化技術(shù)。模型檢驗也終于從學(xué)術(shù)界應(yīng)用到如芯片檢測、通信協(xié)議、外部設(shè)備主控軟件、嵌入式系統(tǒng)（如在飛機、火車、火箭、衛(wèi)星或移動電話）以及安全算法等工業(yè)檢測領(lǐng)域。

雷鋒網(wǎng) AI 科技評論發(fā)現(xiàn)，上面提及的嵌入式系統(tǒng)「碰巧」是 Joseph Sifakis 于 1993 年創(chuàng)辦的 Verimag 實驗室的主攻研究。自 1998 年起，Sifakis 就積極推動嵌入式系統(tǒng)面世并為該領(lǐng)域的國際和現(xiàn)場研究社區(qū)的組建作出了貢獻。他一直擔任 ARTIST 歐洲嵌入式系統(tǒng)設(shè)計卓越網(wǎng)絡(luò)的科學(xué)家協(xié)調(diào)員（Scientific Coordinator），幫助協(xié)調(diào)歐洲領(lǐng)先的嵌入式系統(tǒng)團隊。Sifakis 積極協(xié)助在歐洲成立 ARTEMISIA 嵌入式系統(tǒng)工業(yè)協(xié)會，同時他還是 EmSoft 會議和嵌入式系統(tǒng)周的聯(lián)合創(chuàng)始人。

近幾年，隨著計算機整體技術(shù)水平的發(fā)展，被公認為與人工智能，AR/VR 并列未來三大主流技術(shù)的物聯(lián)網(wǎng)，即信息物理融合系統(tǒng)（Cyber－Physical System），物聯(lián)網(wǎng)系統(tǒng)（Internet of Things）的重要地位愈發(fā)凸顯，而將模型檢測推向應(yīng)用的 Joseph Sifakis 不止用該自動驗證技術(shù)保證了航空，軍工等安全攸關(guān)行業(yè)的安全落地發(fā)展，還對物聯(lián)網(wǎng)的基礎(chǔ)支撐技術(shù)：嵌入式系統(tǒng)深有研究，未來隨著物聯(lián)網(wǎng)應(yīng)用的進一步落地，我們也將面臨更加復(fù)雜的傳感器，通信等技術(shù)，這也將對更加復(fù)雜和開放嵌入式系統(tǒng)進行驗證帶來的新挑戰(zhàn)，屆時如何避免悲劇，保證系統(tǒng)安全就顯得至關(guān)重要。

雷鋒網(wǎng) AI 科技評論了解到，Joseph Sifakis 在去年 9 月的第五屆 HLF（圖靈獎獲得者演講大會）上發(fā)表了針對 IoT 未來的演講。Joseph Sifakis 如此看待 IoT 的未來：

IoT 革命的背后是，對互聯(lián)的智能對象提供的資源管理自動化和增強人們生活質(zhì)量需求的日益增長。IoT 愿景里有智能電網(wǎng)、智能交通系統(tǒng)、智能衛(wèi)生保健服務(wù)、自動化銀行服務(wù)、智能工廠等等，其中智能化互聯(lián)對象之間的協(xié)調(diào)就顯得至關(guān)重要。要實現(xiàn)該 IoT 愿景，我們有著長期內(nèi)需跨越的技術(shù)障礙，同時也要認識到現(xiàn)階段的基礎(chǔ)設(shè)施網(wǎng)絡(luò)并不安全也不保險，這就需要發(fā)展混合關(guān)鍵性系統(tǒng)的設(shè)計流程。

看到這里，想必你也跟 AI 科技評論達成了共識：從模型檢測到嵌入式設(shè)備，再到物聯(lián)網(wǎng)時代，Joseph Sifakis 最有話語權(quán)。

第三屆 CCF-GAIR 全球人工智能與機器人峰會將于 6 月 29 日-7 月 1 日席卷鵬城，屆時將會有 1 個主會場和 11 個專場（仿生機器人專場，機器人行業(yè)應(yīng)用專場，CV 專場，智能安全專場，金融科技專場，自動駕駛專場，NLP 專場，AI+ 專場，AI 芯片專場，IoT 專場，投資人專場），意欲從產(chǎn)學(xué)研多個維度，呈現(xiàn)出更富前瞻性與落地性的會議內(nèi)容。

而 Joseph Sifakis 也將作為重磅嘉賓蒞臨現(xiàn)場并帶來主題演講，所以你確定不來當場了解一下圖靈獎得主 Joseph Sifakis 的最新研究與思考嗎？目前四折門票正在火熱銷售中，限量 100 張，詳情可訪問大會官網(wǎng)了解。

官網(wǎng)：https://gair.leiphone.com/gair/2018yr 

雷峰網(wǎng)原創(chuàng)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。