自動驗證技術獲得圖靈獎

三人分享圖靈獎

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

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

自動驗證用途廣

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

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

模型檢測是核心

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

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

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

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

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

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

實時系統也用上

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

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

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