返回首页
当前位置: 主页 > 教育技术学 > 资源收藏 >

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

时间:2012-02-15 13:41来源:知行网www.zhixing123.cn 编辑:麦田守望者

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

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

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

 

  下面我就讲可预计的软件,这也是有想法在里面的,这和前头相比不如那个那么宏伟,但是更加实际,我主要想对在座的学生讲这些内容,因为希望你们能够面临我们研究的一些挑战,使我们的软件更加有个性,就这个问题使你们能够兴奋起来。软件应该是无“数”不在的,不能对软件周围画一条线,它周围应该是有小的应用程序母本构成的,还有大的一些东西,包括操作系统数据库,很难定起来难以找到的东西,比如移动编码当然是永远存在的,但是是有记录的。很难找到谁是这个软件的写者,令人不能相信的是不能知道来源和创造者,同时也是认证的编码,所以相信是第三方的编码。不久就会有一些这样的图画,我会逐渐把这个变得更大。这是医院的一个病人,给他输液,输液管道是由软件控制的,医院的病人也是有专门的房间,同时医生也带着PDA走来走去,另外还有一个远程病房会有医院档案记录的地方,比如记录一下这个病人花了多少钱。同时医生也可以拿着手机开着车远程对病人治疗情况进行监护。这个远大想法并不是不太现实,我们不久就会看到这些,可能还会很快看到,问题就是到处都有很多软件,我们如何相信软件能够把工作做好。有一些非常有意思的想法和评论,一个是嫁接系统,这种系统在关键系统当中是有的,特别是控制性的软件来确定是不是做了某些移植,在核反应堆控制系统当中也是用这种软件,在智能汽车、智能高速公路上都用这样的系统,这是多样通讯系统,涉及到很多不同的装置,包括使用什么样的机制、什么样的协议,我们到处都可以看到分布式的系统,每天都可用,并且可靠安全。前面也讲到隐私的问题,要使得隐私在表决票上加以保护是很难的。关于人机界面这一块,要注意到社会上能够接受。最后,所有人都注意到我们今天做的这些事情都会需要面对,甚至是更多这方面的问题,也许今后的问题会更加大了。

  我想讲一下多重系统这方面的挑战,嫁接混合系统这方面环境是多重的、难以预测的,这个环境的复杂性是由于自然造成的,有些非常复杂的东西要做模拟,还有一些不同的变量都要加以反映。系统完整性的特点不是考虑到功能了,要使得计算能够更具有出色的结果,但是根据其他资源的限制还要考虑到硬件。看这张关于混合系统,比如说刚才那张照片,都可以意识到非常复杂。怎么保证这一点,到处都用的软件有什么影响,一个是纸张问题要加以保证,当然还有可靠性,除了可靠性之外还有安全的问题,在我们的编码当中还有很多方面。我认为安全性、可靠性、可用性这几个问题就构成了令人可相信的计算组成部分,微软公司可以说在这方面是领导公司之一,领导着令人可以置信的计算,领导着我们的软件发展。到处都有软件,这还有什么影响?我们如何来确定这些特点如何拥有的,对软件体系做一个什么样的定位,性能很好以及正确这两个方面我们说了几十年了,正确就是对不对,性能就是快不快,我想正确性和性能还是不够的,我们是否能够实施可信赖的技术。什么叫正确和信赖,这意味着什么,这个听起来不错,是不是可以及时做正确的事情,比如说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系统,然后把原先的进行界定,之后找到你的反例子,最后对模型进行测验,如果没有对应的途径的话,就要继续去找。你要确定在抽象当中所找到的例子是可以用不同的技巧做到的,可以用不同的方式,更重要的是你可以用不同的技术,只是审查反例子当中的一部分就可以了,因此我们把技巧适用于那种平常性的控制。

------分隔线----------------------------
标签(Tag):周以真 卡内基梅隆大学
------分隔线----------------------------
推荐内容
猜你感兴趣