林惠民

简介: 林惠民,男,1947年生,福州人。1982年毕业于福州大学计算机科学系。1986年获中国科学院软件研究所博士学位。中国科学院软件研究所研究员。长期从事计算机程序的形式语义学及形式化方法的研究。1999年当选为中国科学院院士。 他的工作获得1996年度中国科学院自然科学奖一等奖和1999年度国家自然科学奖二等奖。
[展开]

林惠民的个人经历

1982年毕业于福州大学计算机科学系。1986年获中国科学院软件研究所博士学位。中国科学院软件研究所研究员。长期从事计算机程序的形式语义学及形式化方法的研究。设计并实现了通用进程代数验证工具PAM/VPAM,对这类工具的发展产生了重要影响。与英国Hennessy教授合作提出,并独立发展了“符号互模拟”理论,解决了传统并发计算模型对大量实际应用不能有效模拟的问题,为在计算机上对通信并发进程进行推理和验证提供了理论依据。提出并发计算模型之一π-演算弱互模拟的完备证明系统和唯一不动点归纳法,解决了π-演算的有穷公理化问题。1999年当选为中国科学院院士。

林惠民 - 人物简介

林惠民,1947年11月生于福建省福州市,研究员,博士生导师。1986年在中国科学院软件研究所获博士学位;曾先后在英国爱丁堡大学和萨塞克斯大学工作。1999年被评为“国家级有突出贡献的中青年专家”,同年11月当选为中国科学院院士。主要研究方向包括:通迅并发系统的理论、工具及应用、模型检测、代数规约、程序模块化理论。

他长期从事并发理论及形式化方法的研究。他设计并实现的交互式证明系统PAM是世界上第一个通用的进程代数验证工具。与国际同行合作提出、并独立发展了传值并发进程的“符号互模拟”理论;解决了π-演算和时间自动机的有穷公理化问题。这些成果已为国内外同行在公开发表的文献中所广泛引用,推动了这些领域的发展。他的工作获得1996年度中国科学院自然科学奖一等奖和1999年度国家自然科学奖二等奖。

林惠民

林惠民研究员,1947年11月13日生于福建省福州市。1982年2月在福州大学计算机系计算机软件专业获得学士学位;1986年6月在中国科学院软件研究所获得计算机科学理论专业博士学位。林惠民研究员长期从事计算机程序,特别是并发程序的形式语义学及形式化方法的研究。他在进程代数的验证工具、消息传送进程的语义理论和π-演算的公理化等方向上取得了突破性进展,其主要贡献包括:1996年林获中国科学院自然科学一等奖(唯一获奖人)。他学风严谨,勇于开拓创新,取得了一系列国际领先水平的成果,受到国际同行的公认,是在国际上有影响的计算机科学家。

林惠民 - 重要贡献

林惠民研究员长期从事计算机程序,特别是并发程序的形式语义学及形式化方法的研究。他在进程代数的验证工具、消息传送进程的语义理论和π-演算的公理化等方向上取得了突破性进展,其主要贡献包括:

1.设计并实现了世界上第一个通用的进程代数验证工具

进程代数的实际应用离不开计算机辅助工具的支持。八十年代后期,一批进程代数验证工具应运而生(如CWB,PSF,LOTOSphere等),其共同局限性是每一工具只适用于某一特定的进程演算。这种局限性妨碍了验证工具的推广应用。如何克服这种局限性是当时国际进程代数界面临的一个重大挑战。  这些验证工具无法做到通用,根本原因在于缺乏既能描述不同进程演算的语义,又能为计算机所理解的通用语言。经过对不同演算的反复比较,并考虑到在计算机上实现的可能性,林提炼出了一个元语言,用它可以描述各种进程演算的公理化语义,并且具有良好的可读性。在此基础上实现了通用的交互式进程代数验证工具PAM[1],只要将这个元语言描述的进程演算定义输入PAM,就得到该演算的证明器。PAM可同时接受多个不同的演算,对每个演算又可生成多个证明窗口。这是世界上第一个通用的进程代数证明工具。  1993年林又利用当时刚刚取得的关于消息传送进程证明系统的理论结果,对PAM加以扩充,研制成迄今世界上唯一能对付消息传送进程的验证工具VPAM[2]。

2.与Hennessy教授合作提出、并独立发展了“符号互模拟”理论,在消息传送进程研究中取得突破性进展。

并发理论研究的核心问题是进程间的通讯(消息传送)。可是在传统进程代数的理论研究中,为了数学处理的方便,通讯被简化为单纯的同步。从消息传送进程到单纯同步演算的过渡由一转换完成,其核心步骤是把输入动作翻译成遍历数据域的选择算子。当数据域无穷时,这是个无穷算子,而在实际问题中数据域往往是无穷的。这种无穷算子的引入使得进程代数的很多理论结果无法付诸应用,耗费大量人力物力开发研制的验证工具也难以用于解决实际问题。

林惠民与英国Sussex大学的Hennessy教授合作,提出了“符号互模拟理论”[3],其基本出发点是不依赖上述转换而直接建立消息传送进程的语义理论。这一理论将输入视为一种抽象的动作,而不是将其实例化,从而避免了因数据域无穷而带来的无穷性。这里要克服的主要困难是在执行抽象输入动作后,进程项可能含有自由变量,即成为开项,而传统进程代数理论所使用的语义模型只能解释不含自由变量的闭项。为此[3]中引入了“符号迁移图”作为开项的语义模型,在此基础上建立了符号互模拟理论。在[4]中又进一步建立了消息传送进程互模拟的相对完备证明系统。

3.彻底解决了π-演算的有穷公理化问题

为了描述移动式通讯,ACM图林奖获得者Milner教授与其合作者于1989年正式提出π-演算(也称“移动进程演算”)。π-演算研究中的一个基本问题是刻划进程的互模拟等价关系。π-演算的最初文献中只给出常(ground)强互模拟的公理系统。四年以后,π-演算的提出者之一发表了一般强互模拟的完备公理系统,但没能解决更为困难的弱互模拟的公理化问题。这一问题成为π-演算研究中一个激烈竞争的热点。

林针对π-演算建立了符号互模拟的理论,在95年5月第六届国际软件开发的理论与实践会议上发表了π-演算迟、早两种弱互模拟的完备证明系统[7]。在同年8月美国费城举行的第六届国际并发理论会议上国际同行引用这一成果时指出:“时至今日,π-演算的迟弱互模拟的公理化只在[Lin95]中借助于符号互模拟的概念得到。”(见附件“引用情况摘录”)

为了对π-演算中递归定义的无穷进程进行推理,在第六届国际并发理论会议上林在π-演算中引入“进程抽象”的构造,提出了适用于π-演算的唯一不动点归纳法[8],并进一步于98年7月在第三十五届ICALP大会上发表了有穷控制π-演算弱互模拟的完备证明系统[9]。这一结果彻底解决了π-演算的有穷公理化问题,使我国在这一竞争极为激烈的研究方向上处于国际领先地位。

此外,近年来提供费用邀请林去作专题学术讲座的还有包括法国INRIA、巴黎高师、英国爱丁堡大学、美国宾州大学等十余所欧、美高等学府和科研机构。

林惠民 - 人物采访

主持人:林老师,您是软件专家,你会不会玩游戏呢?为什么?

林老师:不会,游戏软件它有一个特点,首先它是非常好的一个计算机设备,非常快的计算机运行速度,它可以把图像搞得非常漂亮,非常引人入胜。然后计算机的反应速度远远比人要快,所以它可以编得让你,你总是斗不过计算机。那么编游戏软件的人,他主要的任务就是要编得使这个游戏引人入胜,而且要一步一步让你越玩越想玩,这是搞游戏软件的人的活儿,因为他靠这个吃饭,他靠这个卖钱。问题是您能有多少时间拿出来玩?在好几年以前,就有从英国、美国、德国都有一两个小孩玩到二十四小时,通宵达旦,舍不得睡觉,就是入迷到那个地步了,结果出来以后整个人就跨掉了。年轻人没有自制力,所以就很容易在里面就出不来,吃饭都放不开。

主持人:他在大学选择的是计算机专业,应该是更能去玩这个游戏,或者说他要去设计了,他可能更明白这里面的东西,怎么会放弃呢?

林老师:学软件以后,就不大爱玩计算机游戏了。为什么?游戏软件是搞程序搞软件的人编出来的。你自己搞软件你就晓得,这些游戏都是我们同行设计出来的,编出来的。你在那儿玩游戏玩得很起劲,觉得自己很本事,能够把什么打倒,把什么东西吃掉,实际上都是被那些设计软件的人,他想好的圈套,你在里面兜,怎么兜都是被人捉弄的感觉,就是被自己的同行捉弄了。

主持人:刚才我们听了林老师说了这么多对于网络游戏的看法,同学们有没有什么问题想跟林老师来交流的?

学生:林老师您好!我想问您一个问题,就是说我将来致力于去研究游戏软件,如果现在不花时间在这个游戏上面,去了解它有哪些长处,哪些缺点,到我将来想去编游戏软件的时候,我对这个玩家喜欢哪些方面,不喜欢哪些方面,一无所知,就是说我会做起来很困难,您能帮我解答一下这个问题吗?怎么权衡利弊?

林老师:我想这是你真正要做设计游戏软件和玩游戏是不一样的两件事,就像你天天看电视,不等于你将来准备造电视。我想到将来,你首先得把做软件,怎么搞图像,图像处理,图形处理的方法你得学会,然后你要把编软件、写程序这些基本功学会。要学会这些就需要你,这是在大学高年级学的,那么又需要你中学的这些图形图像,很多是数学的东西,你要这些都一层层弄下来,然后等你将来毕业了,比如到一个搞游戏软件的公司去,那时候你真正是去生产软件,和这个玩是很不一样的事。

林惠民 - 学术经历

目前主要研究方向

长期从事计算机程序,特别是并发程序的形式语义学及形式化方法的研究。

学习经历

1982年2月在福州大学计算机系计算机软件专业获得学士学位;
1986年6月在中国科学院软件研究所获得计算机科学理论专业博士学位。

工作经历

1986年9月-1987年12月英国爱丁堡大学计算机科学基础实验室
1988年1月-1990年3月中国科学院软件研究所副研究员专
1990年4月-1993年4月英国Sussex大学ResearchFellow200092
1993年中国科学院软件研究所研究员kaoyangj
1994年中国科学院软件研究所博士生导师112室
1999年中国科学院软件所计算机科学开放研究实验室主任

社会兼职

1990年《软件学报》编委
1994年中国计算机学会理论计算机科学专业委员会副理事长
1997年中国科技大学研究生院兼职教授
1999年《计算机学报》中、英文版编委
研究成果与获奖情况
他在进程代数的验证工具、消息传送进程的语义理论和π-演算的公理化等方向上取得了突破性进展,其主要贡献包括:1996年林获中国科学院自然科学一等奖(唯一获奖人)。他学风严谨,勇于开拓创新,取得了一系列国际领先水平的成果,受到国际同行的公认,是在国际上有影响的计算机科学家。

林惠民 - 代表论著

1.H.Lin,PAM:AProcessAlgebraManipulator.FormalMethodsinSystemDesign,Vol.7,No.3,pp.243-259.1995.KluwerAcademicPublishers.

2.H.Lin,AVerificationToolforValue-PassingProcessAlgebras.IFIPTransactionsC-16:ProtocolSpecification,TestingandVerification,pp.79-92.1993.North-Holland.

3.M.HennessyandH.Lin,SymbolicBisimulations.TheoreticalComputerScience,Vol.138,pp.353-389.1995.Elsevier.

4.M.HennessyandH.Lin,ProofSystemsforMessage-PassingProcessAlgebras.FormalAspectsofComputing.Vol.8,pp397-407.1996.Springer-Verlag.

5.H.Lin,SymbolicTransitionGraphwithAssignment,Proc.7thInt.Conf.onConcurrencyTheory,Pisa,Italy,August26-29,1996.LectureNotesinComputerScienceVol.1119,pp.50-56.Springer-Verlag.

6.H.Lin,"On-the-flyInstantiation"ofValue-passingProcesses.Proc.JointInternationalConferencesonFormalDescriptionTechniquesforDistributedSystemsandCommunicationProtocolsandProtocolSpecification,TestingandVerification,Paris,France,November1998.pp.215-230.KluwerAcademicPublishers.

7.H.Lin,CompleteInferenceSystemsforWeakBisimulationEquivalencesinthepi-Calculus.Proc.6thInternationalJointConferenceonTheoryandPracticeofSoftwareDevelopment,Aarhus,Denmark,May1995.LectureNotesinComputerScience,Vol.915,pp.187-201.Springer-Verlag.

8.H.Lin,UniqueFixpointInductionforMobileProcesses.Proc.6thInternationalConferenceonConcurrencyTheory.Philadelphia,U.S.A.,August1995.LectureNotesinComputerScience,Vol.962,pp.88-102.Springer-Verlag.

9.H.Lin,CompleteProofSystemsforObservationCongruencesinFiniteControlpi-Calculus.Proc.of25thInternationalColloquiumonAutomata,LanguagesandProgramming,Aalborg,Denmark,July1998.LectureNotesinComputerScienceVol.1443,pp.443-454.Springer-Verlag.

10.H.Lin,ProceduralImplementationofAlgebraicSpecifications.ACMTransactionsonProgrammingLanguagesandSystems,Vol.15,No.5,pp.876-895.1993.ACMPress.

林惠民 - 人物语录

数学。这个名字不好。我念小学那个书叫算术,不叫数学,这是很有我们中国特色的,并且是跟计算机紧密联系在一起的。算术就是它教你怎么做计算的办法,比如算多位数乘法,那怎么做呢,你就有一套方法,你要背九九表,然后你就知道。比如说你是142乘上98,你就知道怎么对斜位,老师就教你这条规则了,个位跟个位乘,然后乘数的个位再跟被乘数的十位数乘,然后你要记住进位,这些都是机械的规则,所谓机械的规则就是计算机能懂,计算机是机械的东西,它不像人一样,有脑袋,那么聪明,计算机是很笨的,它只会做这些机械的事,你要把你要做的事情分解成非常机械的步骤告诉他它。所以你会做乘法,会做除法你就会编程序了。

觉得在中学甚至小学从事计算机教育是非常重要的事情,因为整个社会将来都普及计算机,没有一个人将来能够离开计算机而生活,因为不是所有同学将来都能够到大学计算机系,即使上大学,也只有少量的到计算机系,所以中小学生的计算机教育普及工作极为重要,对整个社会的发展,将来非常重要,对学生将来毕业以后走向社会,能够适应新的信息社会的挑战,这是关键的一步。至少我自己回想起来,越年轻的时候算法思想越好,思维方式越是适应编程序,所以我刚才想到算术,我记得小时候学数学就是想怎么做,我怎么一步步把它做出来,那么到了中学以后,可能就有一些不一样,中学就学代数、几何,代数中国有传统,几何基本上是欧洲来的,它涉及到分析推理的那些训练,我的理解,几何对我的训练,主要是训练我思维的严谨性,所以这个我想是一个事情的两个方面。就是你有算法的思想,你怎么做,你一步一步做出来,把一个复杂的问题分解成机械的步骤。另外一个就是你要有严谨的思路,你分解完以后你应该能够做出来最后是对的。我觉得同学们编程序的时候,把自己尽量变得傻瓜一点儿,就跟计算机差不多一样傻,你就能编好了。

有各方面的原因,一个就是从工作上,那我第一次出国,我当时觉得可能英国人,西方人很了不起,现代的一些计算机这些理论都是他们研究出来的,所以我想他们应该是很了不起的,好像比我们会怎么样,比我们中国人可能脑袋里面什么东西,结构不大一样,是不是比我们丰富一些。但是跟他们接触以后,我觉得也不是那样,作为人来说,没有什么大的差别。1987年底那时候我生父去世了,所以这对我触动很大,我想我应该回来,我能做的事情带回来一样做。

林惠民 - 相关词条

梁思礼 匡定波 李衍达 雷啸霖 林尊琪
干福熹 黄宏嘉 李启虎 陆汝钤 刘盛纲
郭雷 黄民强 李未 侯洵 刘永坦
郭光灿 黄琳 简水生 李志坚 刘颂豪
高庆狮 何积丰 侯朝焕 林惠民 阙端麟

 

 

 

 

林惠民 - 参考资料

1、http://www.ios.ac.cn/viewArticle.actionarticleId=122

2、http://hi.baidu.com/johnllon/blog/item/ea0a028d3314d311b31bba15.html

更新日期:2024-04-29