图文：卡内基梅隆大学计算机系主任周以真演讲

图为：卡内基梅隆大学计算机系主任周以真教授演讲。(骆磊 摄)
点击此处查看全部科技图片

　　新浪科技讯 11月1日，第七届“二十一世纪的计算”大型学术研讨会在杭州召开。届时国际著名的计算机大师包括图灵奖获得者、美国国家工程院院士及美国国家科学院院士等多位著名科学家莅临大会。会议由国家自然科学基金委员会、微软亚洲研究院、杭州市人民政府以及浙江大学联合举办。

　　图为：卡内基梅隆大学计算机系主任周以真(Jeannette Wing)教授演讲。(骆磊 摄

)

　　以下为其演讲全文：

　　Jeannette Wing：大家早晨好！非常荣幸能够今天早上到这里为这么多公众以及非常优秀的人士发言，我想感谢微软组织了这次会议，也要感谢浙江大学，以及感谢地方官员，作为东道主在杭州这个美丽的城市举办这个会议。

　　我保证我要讲的是可预测的软件，这基本上是一个摘要，但是我想借此机会向在座的学生、系主任、校校长、计算机科学的研究人员，本着这次会议的主题，也就是“二十一世纪的计算”来介绍一下我的想法，这一点也是与计算机科学有关的。开始的时候我先用一分钟跟大家讲一下计算的讲法，之后讲一下可预见的软件。

　　我对这个领域总的想法是这样的，计算机科学要超过任何行政、任何国家的边界，这是我对于计算机科学的一个远大想法。计算机应该是在二十一世纪中期每个人都应该掌握的一个技能，就像读书写字一样，这也是我的梦想。大家可以想象每个孩子都知道如何像计算机科学家那样思考，这会是怎样的世界呢？要实现这个梦想，计算和计算机就要一起来工作，我要给大家讲一下计算思维的例子。每一次面对一个问题的时候我们都要面对一个问题，这个问题的难度有多大，每一次我们都有精确的问这个问题的方式，也有回答这个问题的方式。计算的想法就是把看来更加困难的问题换成一种我们知道是如何解决的问题，通过嵌入、转换、模拟等等，计算的方法就是选择一个适当的代表或者模型反映出这个问题的有关方面，使得它有不可更总性，计算的想法就是把解决复杂的问题分开来解决，同时也要判断它的设计和好处，简单化。同时也要检查分析多面的一般化的问题，计算机的思维就是要防止出现最大问题的时候如何恢复，这种东西也涉及到多用户，这也涉及到僵局，然后是涉及到解决非常难的人们的困难等等。总的来说，计算机思维就是采取方法解决问题，并且理解人类的行为，而且是和计算机科学非常关键的一些想法，有些计算机思维最喜欢的例子你也可以告诉我们。在学习方面，计算机思维也使得统计问题革命化了，美国的一些统计部门也在用计算机科学家，因为他们知道今后他们的未来在这个职业。美国的计算机学院也开始拥抱现有的部门了，我们的梅隆大学和微软公司开展了合作，我们认为算法和结构以及计算机思维方式将有助于生物学的发展。也有专家在游戏理论以及计算机方面进行广泛的研究。

　　下面我就讲可预计的软件，这也是有想法在里面的，这和前头相比不如那个那么宏伟，但是更加实际，我主要想对在座的学生讲这些内容，因为希望你们能够面临我们研究的一些挑战，使我们的软件更加有个性，就这个问题使你们能够兴奋起来。软件应该是无“数”不在的，不能对软件周围画一条线，它周围应该是有小的应用程序母本构成的，还有大的一些东西，包括

　　我想讲一下多重系统这方面的挑战，嫁接混合系统这方面环境是多重的、难以预测的，这个环境的复杂性是由于自然造成的，有些非常复杂的东西要做模拟，还有一些不同的变量都要加以反映。系统完整性的特点不是考虑到功能了，要使得计算能够更具有出色的结果，但是根据其他资源的限制还要考虑到硬件。看这张关于混合系统，比如说刚才那张照片，都可以意识到非常复杂。怎么保证这一点，到处都用的软件有什么影响，一个是纸张问题要加以保证，当然还有可靠性，除了可靠性之外还有安全的问题，在我们的编码当中还有很多方面。我认为安全性、可靠性、可用性这几个问题就构成了令人可相信的计算组成部分，微软公司可以说在这方面是领导公司之一，领导着令人可以置信的计算，领导着我们的软件发展。到处都有软件，这还有什么影响？我们如何来确定这些特点如何拥有的，对软件体系做一个什么样的定位，性能很好以及正确这两个方面我们说了几十年了，正确就是对不对，性能就是快不快，我想正确性和性能还是不够的，我们是否能够实施可信赖的技术。什么叫正确和信赖，这意味着什么，这个听起来不错，是不是可以及时做正确的事情，比如说Google是已经不错的结果了，但这还不行，对于Google来说并不需要结果是完全准确的，只是需要这些差不多的回答第一时间出现在浏览器上面就行了，但是在技术方面还是不够的。我们应该尝试可预测性的标签，是否可预测，意思就是说正确的行为、而且是可接受的行为，和不可接受的行为，而且可预测可接受，这是由最终用户，是人或者机器来决定的，当然不同的用户之间对这个有不同的界定。这些方法我已经用了很多年，你必须从一个体系的模型入手，这样的话你可以通过很多的模型进行预测，所以是企业这样的一个方法，这里有两个方面，一个是体系方面的模型，另一方面是他的这种特征，就是你希望这样的体系有什么样的特征，所以两个信息放到两个选择里，而且是自动的，你或者说是或者说不是，你输入的信息是看是否能用，这些检查装置是看这些检查方式你可能会获得一些模棱两可的结果。有时候你的过程不够有力可以是你得到准确的答案。另外企业方面的，你需要具体的说明你想让系统展现的特征，企业方面的另外是一个竞争和谐方面的进程，我们显示这些特征是有效的，对特定的系统模型来说是可行的。如果我想我的客户从中有所获益的话，使他们了解系统要起的作用，或是把核查软件系统进一步的推动，模型核查有很多的好处，速度快，可以处理大量的文件，你不必有一个完整的对特征的具体规格的说明，或者说在做任何的工作之前，不必做很细的规定。那么，他的范围是非常的广。从安全的特点，那么安全性的特点是说不会有任何不好的事，另外，最终一些好的东西可能会出现。我想这个模型核查的主要的优势在于这种核查系统，可以告诉你这些特征的成立或者是不成立，但是他在告诉你不成立的时候，他就会提出一些反对的例子，就是说这种核查的价值，恰恰是为什么说像微软这样的公司使用这种模型核查，因为这些反例子告诉了我们为什么这种软件设计是不对的，他是作为一种消除错误的机制。

　　但是有一个很大的不利之处。就是空间扩展的问题，对模型核查来说，假定你认为你输入的东西，在每次作核查的时候，另外一个人可以说他处理这个系统的时候，他的量比你多，这个量的问题是来源于不同的渠道，比如说有平行错误的时候，你有很多这种线程的控制，比如说在软件区域很丰富的时候，你需要看每一个系统到处理多少的程序。这个问题成为过去20年来模型研究员所关注的对象。

　　比如说分解和分解的技术，还有多模型的技术，这张图显示的是这有两个输入的信息，这两个信息放到黑盒子里面去，他被成为模型检查器，模型的问题是代表一些最后的结果，这些问题是你是否对MS成立。

　　给大家分享一下模型中的一些成功的程式，这是我的学生找到了很多模型的错误，其中很多在获得博士学位的人在80年代就提出了一个理念，94年的时候INTEL公司如何发现Pentium流程的问题。许多公司进行模拟测验，来设计何时可以看到软件的错误。而且最激动人心的故事，最近几年里面由微软公司所做的工作，在2000年的时候，我们的发言人已经讲过的，这些结果非常成功，Bill Gates说在2002年的OOPSLA里面提出的故事。模型核查在过去30年里面取得了很大的进展。

　　这是最近两年的结果，一个是针对我所在的安全性方面的工作，作为模型检查的一种扩展，怎么解决安全性的问题，之后会给大家显示一下我在卡内基大学的同事所表明的一种新的技术，就是把混合模型核查的新系统。

　　模型核查是通过提供反例子告诉你为什么你的系统就某个特定的特征来说是不对的，在我所做的工作里面，我们爱查出所有的反例子，特定的模型和特征不止是一个。这个图从左到右先开始最初的一些状态，之后进入最后的阶段。红色团队是由美国国家实验室建立的，现在在开发这样一种图形，它把红色团队加入进来，告诉他攻击者如何进攻我的体系，它提供一种攻击路线图，这个图的提供是手工做的，这意味着一些不一致性、重叠性，以及一些不完整性。做任何手工工作的时候我们一直在说能否自动来做，这是我和我的学生一直在问的问题，所以我们采用模型核查来自动产生所谓的攻击路线图，反例子就把它形成一种攻击。反例子是来自一系列Stat组成的，这种攻击就形成了一系列的Stat。就是说违反了特定的安全特征的。这是单一的简单反例子，入侵者能够成功的道路。具体来说，在所有的Stat里面入侵者没有获得托管系统的准入。最后的M就是安全特征，攻击违反了行动，所以M是一系列的攻击。

　　我来介绍一系列的办法，我们有M的攻击，以及G的图形。最后一种办法我们用M和G进行计算，然后产生LM和(I)，然后我们得出G，最后我们就形成这样一个G的供给图，这是一种非常简单的算法，然后得出我们所需要的东西。

　　性能很不错，而且是达到了这样一系列的技术。这个例子是我们如何把模型核查扩展到各种各样的反例子里面，然后用到安全性能当中去。下一个例子是新的技术，证明所有的模型核查都是试用的。在这里给大家介绍一下混合体系。这帐技术是专门用于处理大的Stat，尤其是无线Stat。现在有一个具体的系统，M，先得出Mh，如果违反了(I)，你可以继续去找，一直到停止的时候。这里面有个理论，叫做危机理论。如果能够满足(I)的话，那就证明最初的模型M能够满足(I)。这项技术已经在硬件里面得到使用，尤其在核查的时候得到了应用，以及其他一些例子得到了应用。我给大家显示的例子是一种混合的系统，混合系统属于无线系统，你必须处理各种各样的变量、状况，以及气压、气温、流通速度，以及其他一些因素，告诉你处于什么样的模型中。通过这种控制图，一系列的反例子技术肯定有个对应的途径，实际发生的情况是你先开始M系统，然后把原先的进行界定，之后找到你的反例子，最后对模型进行测验，如果没有对应的途径的话，就要继续去找。你要确定在抽象当中所找到的例子是可以用不同的技巧做到的，可以用不同的方式，更重要的是你可以用不同的技术，只是审查反例子当中的一部分就可以了，因此我们把技巧适用于那种平常性的控制。

　　在美国有些高速公路是连接不同城市的，这些高速公路通常上面没有车，或者车是非常少的，这是很难令人置信的一件事情。也许从纽约到西雅图去，或者是开到旧金山去，这个距离比较远了，你坐在车里还是很累的，车上有这么一个功能，你累了时候就按一下按纽，脚就不用加油了，这时候定个寻航，比如70脉，因为前面没有车，你就不用总踩着油门了，这就叫平衡控制。至于说前面没有车，或者是车比较远你不会追尾，这种系统就比较好了，但是在城市里开就不行了，在杭州开就更不行了，在杭州根本就不可能用寻航控制系统。但是美国的一些人会提出，我们会想办法，来找一种适应性的寻航控制，前面有车你离他比较近的时候，而且你的速度在不太安全的情况下，如果你靠他比较近了的话，这时候我们用一种自动方式你的车就会减速，我们把这个叫做适应性的平衡控制系统。

　　这里要确定这个系统当中的一些特点，实际上特点也很简单，没有追尾就行了。我们对这个系统做了一个模拟，是非常简单的一种混合式的系统，你可以看到这里左上角的状况，我会把这个结果再说明一下。在左边可以看到状况，用一种反例子的做法，就是说你可以用刚才检查反例子的一些状况，这时候几乎没有什么要检查的状况，因此这个技术是非常令人兴奋的，我们可以用于一些非常困难风险非常大的系统当中。

　　我给他们提出一个挑战，这并不是软件检查的挑战，软件模型检查为什么变得那么具有挑战性？有哪些因素呢？包括编程语言，以及今后到处都有的软件，这本身就是软件模型的复杂性和挑战性。这里列了这么多问题，这里其中一个有可能会成为你们今后写论文的方向，这些都是值得研究的挑战领域，也是面向我们这个社会的，微软也在解决很多这方面的问题。你可以问一下要检查什么，是检查编码还是检查编码的设计，有些人可能会说，不要去管码了，只要检查设计就好了，因为设计错误了，检查编码也是没有用的。有的人关心的是软件架构模式检查，或者叫审查。我的同事还有一个问题，那些特性如何进行检查，因为今后的软件越来越复杂，他们今后的检查如何进行，我的回答是不止要进行模型检查，模型检查同时要进行动态分析以及审查检查的技巧，因此模型检查只不过是整个工作当中的一部分而已。

　　最后结束之际，我想说的是，我对于上述所有软件的想法要实现的时候都要超出传统的计算机科学领域，包括数学、自然科学、经济学、行为科学，还涉及到用户使用的问题，社会层面的问题，还有公共政策方面的问题，另外还有隐私方面的问题，因此都可以实现软件方面的理想，这就要在计算机科学方面取得关键性的进展，同时也要在计算机以及其他学科相互交叉方面取得巨大的进展。