闵应骅的博客分享 http://blog.sciencenet.cn/u/ymin 一位IEEE终身Fellow对信息科学及其发展的看法

博文

模型检验(结束语)(100101)

已有 4218 次阅读 2010-1-1 15:24 |个人分类:学术导航|系统分类:科研笔记| 工具, 复杂性

模型检验(结束语)(100101)
闵应骅
    学习完模型检验(model checking)三位创建者的文章以后,现在可以说几句结束语了。
    科学大家就是科学大家。他们就模型检验28年来的发展,对历史、研究动机、已有成就及今后发展做了高度的概括和总结,指明了方向。但是,真要想做这方面的研究,还需要就其中的一个问题,查阅文献,深入下去才行。
    当今,在计算机工程与科学领域,困扰我们的一个问题是复杂性。系统很复杂,计算很复杂。但是,真要定义什么叫复杂,倒是一个很困难的问题。计算复杂性有一成套的理论,基于图灵机可计算性,有所谓P问题、NP问题。但是,实际上,一个多项式复杂性的问题可能你算不了。例如解线性方程组是多项式复杂的,但是,13亿人建一个13亿阶的方程组,可能现在的超级计算机也算不了。反过来,NP难的问题,在IC设计与测试领域比比皆是。SAT就是一个典型的NP难问题。对于特定的NP问题,我们完全能够用启发式方法,得到很有效率的解。有些过去望而生畏的问题现在已经有了有效的解。例如,OBDD(有序二进制判决图),测试生成,模型检验等。本人上世纪提出的布尔过程,由于复杂性问题而得不到响应。但是,你想一想,我们现在IC设计与测试中碰到的判决问题、优化问题,哪一个是简单的。计算机发展到如此强大,不就是为了处理复杂问题的吗?所以人类的智慧一定会越来越善于处理复杂问题。
    我想,如果我们请一位博士生,读几篇模型检验的文章,然后写一篇综述,他一定会列出许多模型检验工具,说明它们有哪些功能。林林总总一大堆,内容似乎很丰富。三位大师的文章不是这样的。他们指出的是基础性的问题、前瞻性的问题。这对科学研究才是最有益的。商业工具只是根据基础研究成果,变成大众便于使用的工具。所以,工具一定是要落后于研究的。没有研究出方法来,就不会有工具出现。当然,并不是所有的方法都会变成工具。工业界认为有助于实际问题解决的方法,工业界才会把它变为工具,工具好不好最后要看用户满不满意。所以,研究成果的意义最后还是要工业界说话、要实际说话。实践是检验真理的唯一标准嘛!正因为如此,基础研究一定不能削弱,但又不能追着出成果。产品开发很需要做,但不能代替基础研究。

https://wap.sciencenet.cn/blog-290937-283285.html

上一篇:模型检验(5)(100101)
下一篇:未来互联网体系结构(100103)
收藏 IP: .*| 热度|

0

发表评论 评论 (0 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-3-29 01:04

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部