模型检验(结束语)(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)