三人分享圖靈獎

正當我們忙于抗震救災和準備奧運的時候，2008年6月21日晚，美國計算機協(xié)會(ACM)在舊金山召開了2007年度ACM頒獎盛典。頒布了2007年度圖靈獎、ACM Infosys基金會獎以及人工智能、軟件系統(tǒng)、計算機理論與實踐、計算科學與工程等領域的多個獎項。

2007年度ACM圖靈獎由三位研究人員分享，分別是卡內(nèi)基·梅隆大學的Edmund M.Clarke教授、德克薩斯大學奧斯汀分校的E.AllenEmerson教授和法國Grenoble大學Verimag實驗室的Joseph Sifakis教授，獎金是由英特爾公司和谷歌公司共同提供的25萬美元，以表彰他們“在將模型檢測發(fā)展為硬件和軟件業(yè)中廣泛采用的高效驗證技術上的貢獻”。

自動驗證用途廣

今天，軟件、硬件、網(wǎng)絡的規(guī)模越來越大，例如一個芯片上就有上億個晶體管電路，一個嵌入式系統(tǒng)雖小，也五臟俱全。如果設計出了問題，一旦投產(chǎn)，損失就相當大。如何在設計時就能證明系統(tǒng)正確，或者如何能及時發(fā)現(xiàn)設計中的錯誤呢?

目前，一種成效卓著的自動驗證技術(Automatic Verification Technology)已經(jīng)在硬件和軟件工業(yè)界得到了廣泛的應用，特別是在半導體芯片的設計與生產(chǎn)中得到成功的應用。正如英特爾研究中心副總裁錢安達(AndrewChien)在評價模型檢測技術時所說：“英特爾和整個計算機工業(yè)都從他們的貢獻中直接獲益”。谷歌的高級工程副總裁Alan Eustace也說：“谷歌像其他同時代的技術公司一樣，很大一部分成功都來自于先驅(qū)們的研究貢獻”。這些祝賀與評價充滿了真誠的感激之情。

模型檢測是核心

所謂模型檢測技術(ModelCheeking)，本質(zhì)上是用嚴密的數(shù)學方法來驗證一個設計是否滿足預先設定的需求，從而自動地發(fā)現(xiàn)設計中的錯誤。按照定義，它是一種檢查某一給定模型是否滿足某一邏輯規(guī)則的方法。其中一種重要的驗證方法，就是通過算法來驗證形式化系統(tǒng)，具體方法是驗證由硬件或者軟件設計導出的模型是否滿足通常用模態(tài)邏輯規(guī)則表示的形式化規(guī)范。

說得抽象些，模型檢測的基本思想是用狀態(tài)遷移系統(tǒng)(S)表示系統(tǒng)的行為，用模態(tài)／時序邏輯公式(F)描述系統(tǒng)的性質(zhì)。這樣用數(shù)學問題“狀態(tài)遷移系統(tǒng)S是否是公式F的一個模型”來判定“系統(tǒng)是否具有所期望的性質(zhì)”。

第一位獲獎者克拉克(EdmundMelson Clarke Jr.)1945年7月27日生。本科畢業(yè)于弗吉尼亞大學數(shù)學專業(yè)，接著在杜克大學獲得數(shù)學碩士學位，然后在康奈爾大學獲得計算機博士學位。他曾在杜克大學、哈佛大學以及現(xiàn)在的卡內(nèi)基·梅隆大學任教。CMU有他領導的模型檢測研究團隊。他2005年當選美國工程院院士。

這項研究工作于1981年初創(chuàng)。當時克拉克在哈佛大學當教授，他的博士研究生正是第二位獲獎者愛默生(E.AllenEmerson)，他們受到牛津大學計算機科學家霍爾(C.A.R.Hoare)70年代在CACM發(fā)表的一篇論文“Proof ofProgram：Find”(程序證明：發(fā)現(xiàn))的啟發(fā)，走上了形式化驗證的道路。愛默生擁有得克薩斯大學奧斯汀分校數(shù)學學士和碩士學位，并且在哈佛大學獲得應用數(shù)學博士學位。他的博士論文就是為證明程序正確性提供了算法的形式方法。

1982年，克拉克還實現(xiàn)了第一個模型檢測程序。但是，模型檢測方法的缺點是狀態(tài)爆炸問題，導致最初的模型檢測只能應用于很小規(guī)模的設計，從而無法走向業(yè)界。

愛默生對驗證有限狀態(tài)的并行程序做了一系列的工作。1987年，克拉克、愛默生、布瑞安特(Randal E.Bryant，CMU教授)、麥克米倫(Kenneth McMillan，克拉克的博士生)在運用二叉決策圖(BDD，binarydecision diagram)表示符號信息的基礎上，發(fā)明了一種新的模型檢測實現(xiàn)方法，即所謂的符號模型檢測(Symbolic Model Checking)，突破了該方法的規(guī)模和復雜度限制，從而使模型檢測開始廣泛應用于工業(yè)界，尤其是半導體制造業(yè)。為此，他們四人獲得了1998年ACM Paris Kanellakis獎。

實時系統(tǒng)也用上

第三位獲獎者約瑟夫·希法基斯(Joseph Sifakis)是法國Grenoble大學的嵌入式系統(tǒng)研究中心Verimag實驗室的創(chuàng)始人，現(xiàn)在是法國國家科學研究中心(Centre National de la RechercheScientifique)的研究總監(jiān)和CARNOTInstitute on Intelligent Software andSystems in Grenoble的負責人。他在雅典技術大學獲得電機工程學位，在Grenoble大學獲得計算機科學博士學位。

Sifakis和J.P.Queille在法國獨立完成了模型檢測方法的研究，并與Thomas A.Henzinger、Sergio Yovine將該方法應用于實時系統(tǒng)的驗證。

總之，在過去的25年間，這三位圖靈獎得主通過模型檢測為自動驗證奠定了堅實的基礎，使得芯片、硬件、軟件以及網(wǎng)絡的可靠性有了很大的提高。他們創(chuàng)造了計算機輔助驗證CAV(Computer AidedVerification)，正像大家熟悉的計算機輔助設計CAD、計算機輔助制造CAM那樣，積極推動著計算機科學技術的發(fā)展。