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

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

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

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

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

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

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

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

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

嚴(yán)密系統(tǒng)設(shè)計(jì)（Rigorous System Design）

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

Component-based Construction – BIP

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

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

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

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

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

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

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

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

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

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

近幾年，隨著計(jì)算機(jī)整體技術(shù)水平的發(fā)展，被公認(rèn)為與人工智能，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 不止用該自動(dòng)驗(yàn)證技術(shù)保證了航空，軍工等安全攸關(guān)行業(yè)的安全落地發(fā)展，還對物聯(lián)網(wǎng)的基礎(chǔ)支撐技術(shù)：嵌入式系統(tǒng)深有研究，未來隨著物聯(lián)網(wǎng)應(yīng)用的進(jìn)一步落地，我們也將面臨更加復(fù)雜的傳感器，通信等技術(shù)，這也將對更加復(fù)雜和開放嵌入式系統(tǒng)進(jìn)行驗(yàn)證帶來的新挑戰(zhàn)，屆時(shí)如何避免悲劇，保證系統(tǒng)安全就顯得至關(guān)重要。

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

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

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

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

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

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

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