林惠民

林惠民

中國科學院軟體研究所研究員,電腦科學國家重點實驗室主任。長期從事電腦程式的形式語義學及形式化方法的研究。設計並實現了通用進程代數驗證工具PAM/VPAM,對這類工具的發展產生了重要影響。與英國Hennessy教授合作提出,並獨立發展了"符號互模擬"理論,解決了傳統並發計算模型對大量實際套用不能有效模擬的問題,為在電腦上對通信並發進程進行推理和驗證提供了理論依據。提出並發計算模型之一π-演算弱互模擬的完備證明系統和唯一不動點歸納法,解決了π-演算的有窮公理化問題。1999年當選為中國科學院院士。

  • 中文名稱
    林惠民
  • 出生地
    福建省福州市
  • 出生日期
    1947年11月
  • 職業
    中國科學院軟體研究所研究員
  • 畢業院校
    福州大學數學與電腦科學系

生平

人物簡介

1947年11月生于福建省福州市,研究員,博士生導師,電腦科學國家重點實驗室主任。1986年在中國科學院軟體研究所獲博士學位;曾先後在英國愛丁堡大學薩塞克斯大學工作。1999年被評為"國家級有突出貢獻的中青年專家",同年11月當選為中國科學院院士。主要研究方向包括:通迅並發系統的理論、工具及套用、模型檢測、代數規約、程式模組化理論。

林惠民林惠民

工作經歷

他長期從事並發理論及形式化方法的研究。他設計並實現的互動式證明系統PAM是世界上第一個通用的進程代數驗證工具。與國際同行合作提出、並獨立發展了傳值並發進程的"符號互模擬"理論;解決了π-演算和時間自動機的有窮公理化問題。這些成果已為國內外同行在公開發表的文獻中所廣泛引用,推動了這些領域的發展。他的工作獲得1996年度中國科學院自然科學獎一等獎和1999年度國家自然科學獎二等獎。他在進程代數的驗證工具、訊息傳送進程的語義理論和π-演算的公理化等方向上取得了突破性進展,其主要貢獻包括: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大學ResearchFellow

1993年中國科學院軟體研究所研究員

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.

抨擊造假

對于科技界的造假謀取虛名者,林惠民給予了毫不客氣的抨擊。"對科學進步獎,我現在確實沒法相信了。"在2010年全國政協科技和科協界別聯組討論會上,林惠民委員一語驚會。這位62歲的中科院院士、權威的電腦軟體與理論專家說他曾獲邀評審某項目,結果卻發現報獎材料內容是虛假的。林惠民呼呼吁:要加大力度,徹底改革科技獎項評選機製,結束當前的造假獲獎亂象,從而維護科技獎勵的公信力,實現科技評價體系的公平公正,否則,將嚴重挫傷科研人員的積極性,損害國家的創新精神。

林惠民說,"現在拿一個獎去推銷,連企業家都懷疑,人家會問:你們花了多少錢評這個獎?"

林惠民的話引起了廣泛的共鳴。有委員說,對于科技獎存在的問題,社會公眾已經心知肚明,這是很糟糕的事情。委員們的這種體會,在科技界普遍存在。九三學社主要面對高校教師和科研院所的科技人員做了一次調查,在7699份有效樣本中,70.3%的被調查者認為目前我國科技成果的鑒定和評獎結果"既取決于成果的水準,也需要一定的公關活動",僅有12.5%的人認為"主要取決于成果的真實水準"。

行業專家說,歷年來,國家最高科技獎和三大獎的一等獎基本沒什麽爭議,有爭議的是下面的獎項,"這說明數量多了,質量也沒那麽高了,即使沒有造假,咱們國家的科技水準就真有那麽高嗎?雖然報獎材料裏這個寫達到了世界先進水準,那個說解決了世界級難題,但這些獎項又有哪些能拿到國際上比?實際上有水分。"現在的問題是,由行業協會、學會和社會組織評出的獎項也難以服眾。問題的根子在于學術共同體的過度行政化,行政人員不了解學術共同體內的情況,隻能用量化的標準去衡量,而科研人員又不得不跟從,因為行政人員掌握著資源的分配權。

人物語錄

數學。這個名字不好。我念國小那個書叫算術,不叫數學,這是很有我們中國特色的,並且是跟電腦緊密聯系在一起的。算術就是它教你怎麽做計算的辦法,比如算多位數乘法,那怎麽做呢,你就有一套方法,你要背九九表,然後你就知道。比如說你是142乘上98,你就知道怎麽對斜位,老師就教你這條規則了,個位跟個位乘,然後乘數的個位再跟被乘數的十位數乘,然後你要記住進位,這些都是機械的規則,所謂機械的規則就是電腦能懂,電腦是機械的東西,它不像人一樣,有腦袋,那麽聰明,電腦是很笨的,它隻會做這些機械的事,你要把你要做的事情分解成非常機械的步驟告訴他它。所以你會做乘法,會做除法你就會編程式了。覺得在中學甚至國小從事電腦教育是非常重要的事情,因為整個社會將來都普及電腦,沒有一個人將來能夠離開電腦而生活,因為不是所有同學將來都能夠到大學電腦系,即使上大學,也隻有少量的到電腦系,所以中國小生的電腦教育普及工作極為重要,對整個社會的發展,將來非常重要,對學生將來畢業以後走向社會,能夠適應新的信息社會的挑戰,這是關鍵的一步。至少我自己回想起來,越年輕的時候演算法思想越好,思維方式越是適應編程式,所以我剛才想到算術,我記得小時候學數學就是想怎麽做,我怎麽一步步把它做出來,那麽到了中學以後,可能就有一些不一樣,中學就學代數、幾何,代數中國有傳統,幾何基本上是歐洲來的,它涉及到分析推理的那些訓練,我的理解,幾何對我的訓練,主要是訓練我思維的嚴謹性,所以這個我想是一個事情的兩個方面。就是你有演算法的思想,你怎麽做,你一步一步做出來,把一個復雜的問題分解成機械的步驟。另外一個就是你要有嚴謹的思路,你分解完以後你應該能夠做出來最後是對的。我覺得同學們編程式的時候,把自己盡量變得傻瓜一點兒,就跟電腦差不多一樣傻,你就能編好了。

有各方面的原因,一個就是從工作上,那我第一次出國,我當時覺得可能英國人,西方人很了不起,現代的一些電腦這些理論都是他們研究出來的,所以我想他們應該是很了不起的,好像比我們會怎麽樣,比我們中國人可能腦袋裏面什麽東西,結構不大一樣,是不是比我們豐富一些。但是跟他們接觸以後,我覺得也不是那樣,作為人來說,沒有什麽大的差別。1987年底那時候我生父去世了,所以這對我觸動很大,我想我應該回來,我能做的事情帶回來一樣做。

媒體報道

主持人:林老師,您是軟體專家,你會不會玩遊戲呢?為什麽?林老師:不會,遊戲軟體它有一個特點,首先它是非常好的一個電腦設備,非常快的電腦運行速度,它可以把圖像搞得非常漂亮,非常引人入勝。然後電腦的反應速度遠遠比人要快,所以它可以編得讓你,你總是鬥不過電腦。那麽編遊戲軟體的人,他主要的任務就是要編得使這個遊戲引人入勝,而且要一步一步讓你越越想玩,這是搞遊戲軟體的人的活兒,因為他靠這個吃飯,他靠這個賣錢。問題是您能有多少時間拿出來玩?在好幾年以前,就有從英國、美國、德國都有一兩個小孩玩到二十四小時,通宵達旦,舍不得睡覺,就是入迷到那個地步了,結果出來以後整個人就跨掉了。年輕人沒有自製力,所以就很容易在裏面就出不來,吃飯都放不開。

主持人:他在大學選擇的是電腦專業,應該是更能去玩這個遊戲,或者說他要去設計了,他可能更明白這裏面的東西,怎麽會放棄呢?

林老師:學軟體以後,就不大愛玩電腦遊戲了。為什麽?遊戲軟體是搞程式搞軟體的人編出來的。你自己搞軟體你就曉得,這些遊戲都是我們同行設計出來的,編出來的。你在那兒玩遊戲玩得很起勁,覺得自己很本事,能夠把什麽打倒,把什麽東西吃掉,實際上都是被那些設計軟體的人,他想好的圈套,你在裏面兜,怎麽兜都是被人捉弄的感覺,就是被自己的同行捉弄了。

主持人:剛才我們聽了林老師說了這麽多對于網路遊戲的看法,同學們有沒有什麽問題想跟林老師來交流的?

學生:林老師您好!我想問您一個問題,就是說我將來致力于去研究遊戲軟體,如果現在不花時間在這個遊戲上面,去了解它有哪些長處,哪些缺點,到我將來想去編遊戲軟體的時候,我對這個玩家喜歡哪些方面,不喜歡哪些方面,一無所知,就是說我會做起來很困難,您能幫我解答一下這個問題嗎?怎麽權衡利弊?

林老師:我想這是你真正要做設計遊戲軟體和玩遊戲是不一樣的兩件事,就像你天天看電視,不等于你將來準備造電視。我想到將來,你首先得把做軟體,怎麽搞圖像,圖像處理,圖形處理的方法你得學會,然後你要把編軟體、寫程式這些基本功學會。要學會這些就需要你,這是在大學高年級學的,那麽又需要你中學的這些圖形圖像,很多是數學的東西,你要這些都一層層弄下來,然後等你將來畢業了,比如到一個搞遊戲軟體的公司去,那時候你真正是去生產軟體,和這個玩是很不一樣的事。

數計學院舉辦中國科學院林惠民院士專題報告會

中國科學院林惠民院士專題報告會在數計學院學術報告廳舉行,副校長、數計學院院長範更華、學院黨委書記陳詩銓、副書記初勇、牛牧、副院長徐榮聰、葉東毅和師生代表近200人參加了報告會。報告會由副校長、數計學院院長範更華主持。林惠民院士是我院數學專業的77級校友,1999年當選中國科學院院士。林惠民院士精闢入理的報告讓與會師生如痴如醉,贏得陣陣掌聲,報告會取得圓滿成功。

相關詞條

相關搜尋