模型检验（1）(091230）
闵应骅
    大家承认，计算机领域的ACM图灵奖相当于自然科学的诺贝尔奖。2007年图灵奖授予Edmund M. Clarke，E. Allen Emerson,和Joseph Sifakis。他们创立了模型检验---一种验证技术，用算法的方式确定一个硬件或软件设计是否满足用时态逻辑表述的形式规范。如果不能满足，则提供反例。他们在1981年提出这个方法，经过28年的发展，已经在VLSI电路、通信协议、软件设备驱动器、实时嵌入式系统和安全算法的验证方面得到了实际应用。相应的商业工具也已出现，估计今后将对未来的硬件和软件产业产生重大影响。
    2009年11月CACM发表了三位对模型检验的新的诠释。本人将用几次对他们的诠释做一个通俗的介绍，对我自己也是一个学习的过程。
    Edmund M. Clarke现在是美国卡内基梅隆大学（CMU）计算机科学系教授。E. Allen Emerson是在美国奥斯汀的德州大学计算机科学系教授。Joseph Sifakis是法国国家科学研究中心研究员，Verimag实验室的创立者。



转载本文请联系原作者获取授权，同时请注明本文来自闵应骅科学网博客。
链接地址：https://wap.sciencenet.cn/blog-290937-282516.html

上一篇：虚荣心（091227）
下一篇：模型检验（2）（091231）