圖靈獎得主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）組成的系統。該研究主要聚焦以下三項挑戰：

• 一個異構部件（heterogeneous component）中增量組成的框架。異質性的三個不同來源被認為與交互、執行和抽象相關聯

• 通過構建基本系統屬性的 Correctness-by-construction，例如互斥，無死鎖和進度來最小化後驗驗證

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

在產業界取得矚目成功的圖靈獎成果，模型檢測（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 張，詳情可訪問大會官網了解。

官網：https://gair.leiphone.com/gair/2018yr

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！