自动验证技术获得图灵奖.docVIP

自动验证技术获得图灵奖 三人分享图灵奖br　　br　　正当我们忙于抗震救灾和准备奥运的时候，2008年6月21日晚，美国计算机协会(ACM)在旧金山召开了2007年度ACM颁奖盛典。颁布了2007年度图灵奖、ACM Infosys基金会奖以及人工智能、软件系统、计算机理论与实践、计算科学与工程等领域的多个奖项。br　　2007年度ACM图灵奖由三位研究人员分享，分别是卡内基·梅隆大学的Edmund M.Clarke教授、德克萨斯大学奥斯汀分校的E.AllenEmerson教授和法国Grenoble大学Verimag实验室的Joseph Sifakis教授，奖金是由英特尔公司和谷歌公司共同提供的25万美元，以表彰他们“在将模型检测发展为硬件和软件业中广泛采用的高效验证技术上的贡献”。br　　br　　自动验证用途广br　　br　　今天，软件、硬件、网络的规模越来越大，例如一个芯片上就有上亿个晶体管电路，一个嵌入式系统虽小，也五脏俱全。如果设计出了问题，一旦投产，损失就相当大。如何在设计时就能证明系统正确，或者如何能及时发现设计中的错误呢?br　　目前，一种成效卓著的自动验证技术(Automatic Verification Technology)已经在硬件和软件工业界得到了广泛的应用，特别是在半导体芯片的设计与生产中得到成功的应用。正如英特尔研究中心副总裁钱安达(AndrewChien)在评价模型检测技术时所说：“英特尔和整个计算机工业都从他们的贡献中直接获益”。谷歌的高级工程副总裁Alan Eustace也说：“谷歌像其他同时代的技术公司一样，很大一部分成功都来自于先驱们的研究贡献”。这些祝贺与评价充满了真诚的感激之情。br　　br　　模型检测是核心br　　br　　所谓模型检测技术(ModelCheeking)，本质上是用严密的数学方法来验证一个设计是否满足预先设定的需求，从而自动地发现设计中的错误。按照定义，它是一种检查某一给定模型是否满足某一逻辑规则的方法。其中一种重要的验证方法，就是通过算法来验证形式化系统，具体方法是验证由硬件或者软件设计导出的模型是否满足通常用模态逻辑规则表示的形式化规范。br　　说得抽象些，模型检测的基本思想是用状态迁移系统(S)表示系统的行为，用模态／时序逻辑公式(F)描述系统的性质。这样用数学问题“状态迁移系统S是否是公式F的一个模型”来判定“系统是否具有所期望的性质”。br　　第一位获奖者克拉克(EdmundMelson Clarke Jr.)1945年7月27日生。本科毕业于弗吉尼亚大学数学专业，接着在杜克大学获得数学硕士学位，然后在康奈尔大学获得计算机博士学位。他曾在杜克大学、哈佛大学以及现在 的卡内基·梅隆大学任教。CMU有他领导的模型检测研究团队。他2005年当选美国工程院院士。br　　这项研究工作于1981年初创。当时克拉克在哈佛大学当教授，他的博士研究生正是第二位获奖者爱默生(E.AllenEmerson)，他们受到牛津大学计算机科学家霍尔(C.A.R.Hoare)70年代在CACM发表的一篇论文“Proof ofProgram：Find”(程序证明：发现)的启发，走上了形式化验证的道路。爱默生拥有得克萨斯大学奥斯汀分校数学学士和硕士学位，并且在哈佛大学获得应用数学博士学位。他的博士论文就是为证明程序正确性提供了算法的形式方法。br　　1982年，克拉克还实现了第一个模型检测程序。但是，模型检测方法的缺点是状态爆炸问题，导致最初的模型检测只能应用于很小规模的设计，从而无法走向业界。br　　爱默生对验证有限状态的并行程序做了一系列的工作。1987年，克拉克、爱默生、布瑞安特(Randal E.Bryant，CMU教授)、麦克米伦(Kenneth McMillan，克拉克的博士生)在运用二叉决策图(BDD，binarydecision diagram)表示符号信息的基础上，发明了一种新的模型检测实现方法，即所谓的符号模型检测(Symbolic Model Checking)，突破了该方法的规模和复杂度限制，从而使模型检测开始广泛应用于工业界，尤其是半导体制造业。为此，他们四人获得了1998年ACM Paris Kanellakis奖。br　　br　　实时系统也用上br　　br　　第三位获奖者约瑟夫·希法基斯(Joseph Sifakis)是法国Grenoble大学的嵌入式系统研究中心Verimag实验室的创始人，现在是法国国家科学研究中心(Centre National de la RechercheScientifique)的研究总监和CARNOTInstitute on Intelligent Software andSyst