自動(dòng)驗(yàn)證技術(shù)獲得圖靈獎(jiǎng)

三人分享圖靈獎(jiǎng)

正當(dāng)我們忙于抗震救災(zāi)和準(zhǔn)備奧運(yùn)的時(shí)候，2008年6月21日晚，美國(guó)計(jì)算機(jī)協(xié)會(huì)(ACM)在舊金山召開(kāi)了2007年度ACM頒獎(jiǎng)盛典。頒布了2007年度圖靈獎(jiǎng)、ACM Infosys基金會(huì)獎(jiǎng)以及人工智能、軟件系統(tǒng)、計(jì)算機(jī)理論與實(shí)踐、計(jì)算科學(xué)與工程等領(lǐng)域的多個(gè)獎(jiǎng)項(xiàng)。

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

自動(dòng)驗(yàn)證用途廣

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

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

模型檢測(cè)是核心

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

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

第一位獲獎(jiǎng)?wù)呖死?EdmundMelson Clarke Jr.)1945年7月27日生。本科畢業(yè)于弗吉尼亞大學(xué)數(shù)學(xué)專業(yè)，接著在杜克大學(xué)獲得數(shù)學(xué)碩士學(xué)位，然后在康奈爾大學(xué)獲得計(jì)算機(jī)博士學(xué)位。他曾在杜克大學(xué)、哈佛大學(xué)以及現(xiàn)在的卡內(nèi)基·梅隆大學(xué)任教。CMU有他領(lǐng)導(dǎo)的模型檢測(cè)研究團(tuán)隊(duì)。他2005年當(dāng)選美國(guó)工程院院士。

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

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

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

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

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

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

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