为什么2007年的图灵奖选择了模型检测技术

春峰的个人资料我要去桂林照片日志列表

工具

帮助

日志

排列方式：

为什么2007年的图灵奖选择了模型检测技术

像树一样成长，刚听完俞敏洪的在赢在中国的演讲----------题记

2007年图灵奖授予了在模型检测技术领域的奠基性贡献的科学家：Edmund M. Clarke、E Allen Emerson和Joseph Sifakis三位科学家。

什么是模型检测技术呢？看看wikipedia 上的定义吧：
Model checking is the process of checking whether a given structure is a model of a given logical formula. The concept is general and applies to all kinds of logics and suitable structures. A simple model-checking problem is testing whether a given formula in the propositional logic is satisfied by a given structure.

简单的说：是一套用于判断硬件和软件设计的理论模型是否满足规范的方法。这可真是个抽象的描述，看起来似乎离我们很遥远，遥远的只有像英特尔研究中心副总裁Andrew Chien才能对模型检测技术用一句话来评价：“英特尔和整个计算机工业都从他们的贡献中直接获益”。

那模型检测技术是不是离程序员也很遥远呢？图灵奖作为计算机界诺贝尔奖，如果把奖项颁给一个离程序员很遥远的技术，还真说不过去。

带着这个疑问，我浏览了wikipedia上长长的一窜模型检测技术的项目，还好不出所料，找到了下面几个项目：

1、Java Pathfinder ：是一个用来认证java执行字节代码的系统。类似一个java虚拟机用来检测软件运行状态的验证系统。
2、Mono Model Checker ：跑在mono 开源的.net平台上。用来自动侦查 CIL 字节码错误的程序。目前的版本支持CIL的死锁 deadlocks 和断言冲突 assertion violation 。

3、对于c++ 感兴趣的人还可以看看这两个项目：
State Exploring Assembly Model Checker ， Bounded Model Checking for ANSI-C 。

举个例子吧，在开发中，利用测试库junit 和 dotunit 写测试代码已经逐渐普及开了，比如下面这段：

public void testToppingsOnNewPizza()
{
  Pizza pizza = new Pizza();
  List toppings = pizza.getToppings();
  assert( (toppings.size()==0) );
}

注意上面加黑的这句： assert( (toppings.size()==0) ); 。

这段代码我们用来检测：pizza.getToppings() 的大小是否为0。那么模型检测和上面的测试代码有什么不同呢？

不同点在于：现在的测试库用来判断结果，而模型检测用来判断过程（逻辑）是否符合要求。

我们常说，不但要关注结果，更要关注过程。模型检测就是对过程的关注。

无疑，现在写程序的时候，模型检测的过程，是由广大程序员完成的。如果这个过程可以由机器完成的话？那不是就是实现了自动编程吗？据说word的创始人开发者正在干这样的事儿... ，不知道这个老头有生之年能不能实现他的理想。

当然，我也相信在更高级的人工智能技术中，模型检测技术会大展拳脚。

又是个遥远的事情，洗洗睡吧。

2月19日 23:55 | 写入日志 | 计算机与 Internet

若要添加评论，请使用您的 Windows Live ID 登录（如果您使用过 Hotmail、Messenger 或 Xbox LIVE，您就拥有 Windows Live ID）。登录

还没有 Windows Live ID 吗？请注册

	siberianbutterfly发表: 不好意思,都写完了才发现我认错人了. 把你误认成我的高中女同学了,很不好意思. 打饶了,抱歉抱歉 2 月 21 日
	siberianbutterfly发表: 亲爱的,我发现某人越来越进入工作状态了.是件值得庆祝的事情吧? 2 月 21 日
	xiaoxingrong发表: 昨天我也看了win in china.哈哈 2 月 20 日

引用通告

此日志的引用通告 URL 是：

http://tianchunfeng.spaces.live.com/blog/cns!819E33AA1808A272!385.trak

引用此项的网络日志

日志

为什么2007年的图灵奖选择了模型检测技术

评论 (3)

引用通告