在數(shù)學(xué)世界里綻放異彩

李剛

提起數(shù)學(xué)，是令許多人頗為頭疼的一門學(xué)科：枯燥、乏味似乎為其無形中做了一種隱形的“代言”，但對北京大學(xué)數(shù)學(xué)科學(xué)學(xué)院副教授孫猛來說，卻甘之如飴。他所研究的數(shù)學(xué)也絕非僅限于基礎(chǔ)數(shù)學(xué)，在信息科學(xué)領(lǐng)域造詣頗深的孫猛一直致力于將數(shù)學(xué)引入另一片天地。

數(shù)學(xué)中的奇思妙想

自從接觸到數(shù)學(xué)，孫猛就將數(shù)學(xué)視為自己不可分割的一部分，在和孫猛交談的短短一個多小時中，記者看到了他身上承載著的對于科研的嚴(yán)謹(jǐn)、教學(xué)的負(fù)責(zé)，更了解了他背后不為人知的辛勞和快樂。

1994年，年僅15歲的孫猛被北京大學(xué)技術(shù)物理系錄取，一年后轉(zhuǎn)入數(shù)學(xué)系（現(xiàn)數(shù)學(xué)科學(xué)學(xué)院）學(xué)習(xí)。而20世紀(jì)90年代后期正是信息科學(xué)技術(shù)飛速發(fā)展的一個階段，其中許多問題的解決都需要深厚的數(shù)學(xué)背景，在本科期間的學(xué)習(xí)過程中，孫猛的興趣逐漸從純粹的數(shù)學(xué)理論轉(zhuǎn)向了數(shù)學(xué)與信息科學(xué)的交叉領(lǐng)域。1999年，孫猛獲得推免資格，保送成為應(yīng)用數(shù)學(xué)專業(yè)碩士生，剛剛步入一個新天地的孫猛又走到了一個“十字路口”。據(jù)孫猛回憶，他研究生的導(dǎo)師張乃孝教授所研究的主要領(lǐng)域?yàn)檎Z言相關(guān)的問題，包括程序語言及領(lǐng)域語言等，但經(jīng)過一段時間的學(xué)習(xí)了解后，孫猛發(fā)覺自己真正更感興趣的問題還是集中在數(shù)學(xué)在信息科學(xué)之中的應(yīng)用。所幸，導(dǎo)師給予了他充分的學(xué)術(shù)自由，鼓勵他自己找尋研究方向，并在2002年孫猛選擇繼續(xù)攻讀博士學(xué)位后推薦他去聯(lián)合國大學(xué)國際軟件技術(shù)研究所（UNU/IIST）交流。在UNU/IIST期間，孫猛和來自奧地利Graz工大的Bernhard Aichernig教授等合作，開始了關(guān)于組件技術(shù)的余代數(shù)理論基礎(chǔ)的研究工作。

從20世紀(jì)90年代中后期開始，在計算機(jī)領(lǐng)域?qū)τ啻鷶?shù)理論及其在并發(fā)模型、面向?qū)ο?、模態(tài)邏輯、自動機(jī)理論等問題中的應(yīng)用的研究得到了飛速發(fā)展。荷蘭CWI的Jan Rutten教授提出的泛余代數(shù)理論將計算機(jī)科學(xué)中許多不同的具體行為進(jìn)行抽象，得到了統(tǒng)一的余代數(shù)模型。在深入了解了這一理論之后，孫猛發(fā)現(xiàn)其基于觀察的行為描述與軟件組件的“黑盒”特性極其相符，非常適于作為軟件組件的理論模型，并決定以此作為其博士論文的主題。孫猛在其博士論文中所提出的在余代數(shù)框架下的組件精化理論受到了國際同行和相關(guān)領(lǐng)域?qū)＜业母叨仍u價，發(fā)表在第10屆代數(shù)方法和軟件技術(shù)國際會議上（AMAST2004）的論文被評為該會議唯一一篇“Best Student Paper”。

而統(tǒng)一建模語言（UML）作為被廣泛接受的工業(yè)標(biāo)準(zhǔn)，已經(jīng)成為全世界大學(xué)和各種專業(yè)培訓(xùn)項目中計算機(jī)科學(xué)及工程課程中必不可少的一部分，其最主要的設(shè)計目標(biāo)是使其成為一個通用的建模語言，可供不同領(lǐng)域使用?！暗谀Ｐ筒灰恢碌那闆r下，很容易因模型的沖突而導(dǎo)致最后實(shí)現(xiàn)的錯誤，所以需要對UML中不同的視圖模型給出一個精確的統(tǒng)一形式化語義，能夠在此基礎(chǔ)上檢查不同模型的一致性，這對代碼的自動生成以及開發(fā)后期的系統(tǒng)測試、維護(hù)等工作都會有很大幫助?！睂O猛補(bǔ)充道。在他的博士論文及其后續(xù)工作中，孫猛對UML中的類圖、狀態(tài)機(jī)圖、順序圖、用例圖等多種常用視圖模型使用余代數(shù)給出了一種統(tǒng)一的語義定義框架，并在此基礎(chǔ)上成功給出了UML模型的精化、重構(gòu)等操作的定義及證明方法。

復(fù)雜系統(tǒng)中的協(xié)調(diào)

隨著網(wǎng)絡(luò)技術(shù)的飛速發(fā)展，為保證系統(tǒng)在動態(tài)的開放分布式環(huán)境中順利運(yùn)行，系統(tǒng)各組件之間以及軟硬件之間都需要進(jìn)行緊密協(xié)調(diào)工作。如今，協(xié)調(diào)模型和協(xié)調(diào)語言在計算機(jī)科學(xué)中已經(jīng)得到了廣泛應(yīng)用。在獲得博士學(xué)位并于新加坡國立大學(xué)計算學(xué)院從事了1年的博士后研究之后，孫猛于2006年受到荷蘭數(shù)學(xué)與計算機(jī)科學(xué)研究中心（CWI）的Farhad Arbab教授邀請加入其課題組，開始從事關(guān)于協(xié)調(diào)模型和語言的研究工作。十余年來，孫猛一直關(guān)注著協(xié)調(diào)模型和協(xié)調(diào)語言領(lǐng)域，協(xié)調(diào)模型的自動生成、驗(yàn)證與測試、協(xié)調(diào)模型的擴(kuò)展以及相關(guān)工具的開發(fā)等是他目前研究的重點(diǎn)問題。

歐洲科學(xué)院院士Christel Baier等在2005年提出了一種從自動機(jī)規(guī)范自動生成連接件的方法，但一方面復(fù)雜系統(tǒng)的自動機(jī)規(guī)范難以直接給出，另外該方法的結(jié)果中存在大量冗余的異步通道，從而導(dǎo)致狀態(tài)空間過大，難以對系統(tǒng)進(jìn)行有效驗(yàn)證。孫猛與Christel Baier和FarhadArbab合作，提出了一種從UML的順序圖自動生成協(xié)調(diào)模型的結(jié)構(gòu)化方法，成功克服了這兩個方面的問題，并且給出了該生成方法的正確性證明，這一證明通過給出生成的連接件和UML順序圖兩者的余代數(shù)語義之間的互模擬關(guān)系，保證了生成結(jié)果和順序圖規(guī)范之間的語義的一致性。

通過研究基于協(xié)調(diào)語言Reo的協(xié)調(diào)機(jī)制的理論基礎(chǔ)，以不同軟硬件組件之間的交互問題以及對組件交互行為進(jìn)行組合和協(xié)調(diào)的連接件所支持的系統(tǒng)體系結(jié)構(gòu)為對象，孫猛及其團(tuán)隊與國際同行合作，將Reo語言進(jìn)行了多種擴(kuò)展：通過增加概率和隨機(jī)行為相關(guān)信息，定義了Reo的定量擴(kuò)展，并成功實(shí)現(xiàn)了從定量Reo到連續(xù)時間馬爾科夫鏈的變換，從而可對相關(guān)的概率時序邏輯所描述的性質(zhì)進(jìn)行驗(yàn)證：在主持的國家自然科學(xué)基金青年基金項目“基于Reo的協(xié)調(diào)理論及其在信息物理系統(tǒng)開發(fā)方法中的應(yīng)用”中，通過將微分方程與協(xié)調(diào)語言的結(jié)合，建立了信息物理系統(tǒng)中的連接件形式化模型，并且對信息物理系統(tǒng)中連接件的建模、分析、驗(yàn)證和測試的理論與方法進(jìn)行了研究，這可謂是對信息物理系統(tǒng)的設(shè)計和開發(fā)搭了一架便利“橋梁”，也為具有復(fù)雜結(jié)構(gòu)的信息物理系統(tǒng)的建模、分析和嚴(yán)格開發(fā)提供了更好的理論和方法支持。同時，對混成連接件的可組合性、連接件的測試用例生成方法等相關(guān)問題都進(jìn)行了研究，得到了一系列的成果。

“早在上世紀(jì)90年代，協(xié)調(diào)語言的概念就已經(jīng)被提出，這一問題多年來一直是國際上科學(xué)工作者的研究熱點(diǎn)，也引起了包括生物信息學(xué)、面向服務(wù)計算等眾多相關(guān)領(lǐng)域的關(guān)注。但萬物皆不完美，在研究中，我們認(rèn)識到，雖然協(xié)調(diào)問題的研究在國際上是一個不斷發(fā)展的領(lǐng)域，也已經(jīng)取得了一些成果，但是距離實(shí)際系統(tǒng)，特別是信息物理系統(tǒng)開發(fā)的需要還有很大差距，仍有很多問題亟待研究和解決?！睂O猛如是說道。

在科研這條長滿鮮花又布滿荊棘的道路上，無論時光荏苒，孫猛始終不忘初心，一路砥礪前行。