鑄就理論基石 驗(yàn)證系統(tǒng)邏輯
——記上海交通大學(xué)電子信息與電氣工程學(xué)院特別副研究員符鴻飛

□ 黃 健

“實(shí)踐是檢驗(yàn)真理的唯一標(biāo)準(zhǔn)”，很多軟件、系統(tǒng)在開發(fā)時(shí)都會(huì)進(jìn)行模擬驗(yàn)證，以確保順利運(yùn)行。然而近些年來，模擬驗(yàn)證的短板逐漸凸顯——伴隨著計(jì)算機(jī)的飛速發(fā)展，越來越多超大規(guī)模設(shè)計(jì)出現(xiàn)，對(duì)于這些設(shè)計(jì)來說，仿真挑戰(zhàn)過于耗費(fèi)時(shí)間，從理論上進(jìn)行測(cè)試反而更為合適。這種測(cè)試被稱為“形式化驗(yàn)證”，是一種窮盡式數(shù)學(xué)技術(shù)，其原理是利用數(shù)學(xué)和邏輯的方法來證明計(jì)算機(jī)系統(tǒng)的正確性。

在移動(dòng)互聯(lián)網(wǎng)深刻影響著人類生產(chǎn)生活的今天，保障計(jì)算機(jī)的安全性至關(guān)重要，而這其中的核心課題就是確保計(jì)算機(jī)系統(tǒng)的正確性。由于潛在的漏洞可能導(dǎo)致重大的人身或財(cái)產(chǎn)損失，因此，如何保證關(guān)鍵系統(tǒng)不出現(xiàn)重大漏洞是一個(gè)重要的問題。作為理論計(jì)算機(jī)科學(xué)的一個(gè)重要分支，形式化驗(yàn)證為關(guān)鍵系統(tǒng)組件正確性的自動(dòng)化推理和證明提供了堅(jiān)實(shí)的基礎(chǔ)，因此能夠?yàn)橄到y(tǒng)是否滿足一些關(guān)鍵的正確性質(zhì)作出最強(qiáng)的保證。上海交通大學(xué)電子信息與電氣工程學(xué)院特別副研究員符鴻飛長(zhǎng)期致力于理論計(jì)算機(jī)科學(xué)中的形式化驗(yàn)證領(lǐng)域，在取得一系列原創(chuàng)性理論成果的同時(shí)，他不忘尋求與工業(yè)界實(shí)際相結(jié)合，在理論成果付諸應(yīng)用的道路上展開了諸多探索。

“熱愛是最好的老師”

愛因斯坦曾經(jīng)說過：“我認(rèn)為對(duì)于一切情況，只有熱愛才是最好的老師?！毕啾扔谄渌庠谠?，“熱愛”這一內(nèi)在動(dòng)力往往更為持久有效。自2003年考入上海交通大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)專業(yè)以來，符鴻飛一直對(duì)其專業(yè)領(lǐng)域保持著濃厚的興趣，心無旁騖地投身其中。

回想起進(jìn)入形式化研究領(lǐng)域的原因，符鴻飛表示，在本科求學(xué)期間，他經(jīng)常編寫程序，這是計(jì)算機(jī)專業(yè)學(xué)生的日常，但與別人不同的是，符鴻飛沒有止步于編程。在這個(gè)過程中，他對(duì)如何保證程序編寫的正確性產(chǎn)生了困惑，因此在寫完程序后往往會(huì)反復(fù)讀幾遍以確保其正確性。這樣寫程序的速度很慢，因此，符鴻飛萌生了學(xué)習(xí)如何對(duì)程序進(jìn)行快速驗(yàn)證的念頭。

就這樣，在上海交通大學(xué)讀研期間，符鴻飛選擇了研究理論計(jì)算機(jī)科學(xué)中進(jìn)程理論的傅育熙教授作為自己的導(dǎo)師。在他的指導(dǎo)下，符鴻飛對(duì)一些無窮狀態(tài)進(jìn)程模型的可判定性和計(jì)算復(fù)雜性進(jìn)行了研究，并在互模擬判定及模型檢測(cè)算法方面做出了理論上的貢獻(xiàn)。正是碩士階段的求學(xué)經(jīng)歷讓符鴻飛對(duì)利用數(shù)學(xué)方法證明系統(tǒng)正確性的形式化方法領(lǐng)域產(chǎn)生了興趣。

學(xué)習(xí)的樂趣就是不斷發(fā)現(xiàn)新的感興趣的研究方向，從而不斷開辟新的研究領(lǐng)域。對(duì)形式化方法產(chǎn)生興趣之后，符鴻飛通過國(guó)家公派留學(xué)機(jī)會(huì)找到了該領(lǐng)域著名學(xué)者Joost-Pieter Katoen教授，赴德國(guó)亞琛工業(yè)大學(xué)計(jì)算機(jī)科學(xué)系攻讀形式化方法相關(guān)的博士。讀博期間，符鴻飛主要研究概率系統(tǒng)形式化驗(yàn)證，并獨(dú)立自主地給出了諸多相關(guān)理論問題的基礎(chǔ)算法和計(jì)算復(fù)雜性?；ㄙM(fèi)4年時(shí)間順利拿到博士學(xué)位之后，符鴻飛開展了博士后研究，和奧地利科學(xué)技術(shù)研究院（IST Austria）的Krishnendu Chatterjee教授合作研究概率程序的形式化驗(yàn)證，并發(fā)表了多篇關(guān)于基礎(chǔ)理論的結(jié)果。

盡管在國(guó)外學(xué)習(xí)工作多年，但符鴻飛的心中始終記掛著祖國(guó)和故鄉(xiāng)。他期盼著能回到母校，在求學(xué)多年的環(huán)境中，與敬愛的師長(zhǎng)共事。念念不忘，必有回響。2017年，他成功加入上海交通大學(xué)電子信息與電氣工程學(xué)院，任特別副研究員，一圓心中夙愿。

創(chuàng)立形式化驗(yàn)證新成果

多年來，符鴻飛埋首形式化驗(yàn)證領(lǐng)域，不懈鉆研。從廣義上講，形式化方法是借助數(shù)學(xué)的方法來解決軟件工程領(lǐng)域的問題，主要包括建立精確的數(shù)學(xué)模型及對(duì)模型的分析活動(dòng)。狹義地講，它就是運(yùn)用形式化語(yǔ)言，進(jìn)行形式化的規(guī)格描述、模型推理和驗(yàn)證的方法。近年來，隨著系統(tǒng)越來越復(fù)雜，通過傳統(tǒng)測(cè)試方法越來越難以覆蓋足夠多的系統(tǒng)執(zhí)行路徑。因此，形式化方法為全覆蓋、自動(dòng)化的系統(tǒng)正確性證明提供了一個(gè)行之有效的方法。

形式化方法研究有兩個(gè)重要方向，即模型檢測(cè)和程序驗(yàn)證，符鴻飛在這兩個(gè)領(lǐng)域都取得了原創(chuàng)性成果。

與“離散數(shù)學(xué)”課程學(xué)生合影

模型檢測(cè)是研究如何驗(yàn)證系統(tǒng)模型正確性的研究領(lǐng)域?！昂?jiǎn)單來說，就是通過數(shù)學(xué)建模去證明系統(tǒng)模型具有哪些性質(zhì)。”符鴻飛解釋道。在這方面，他著力研究概率模型檢測(cè)的算法、可判定性和復(fù)雜性，并獲得了一些基礎(chǔ)性理論成果。在模型檢測(cè)算法方面，符鴻飛以獨(dú)立作者身份給出了關(guān)于連續(xù)時(shí)間馬爾可夫過程時(shí)序邏輯的兩個(gè)基礎(chǔ)模型檢測(cè)算法，并發(fā)表在國(guó)際著名形式化驗(yàn)證學(xué)術(shù)會(huì)議FOSSACS、HSCC上。其中，發(fā)表在HSCC上的論文獲得了2013年度最佳學(xué)生論文獎(jiǎng)。在可判定性和計(jì)算復(fù)雜性理論方面，他著力研究離散時(shí)間馬爾可夫過程上關(guān)于互模擬等價(jià)關(guān)系的可判定性和計(jì)算復(fù)雜性，并以獨(dú)立作者或主要貢獻(xiàn)者身份在國(guó)際著名理論計(jì)算機(jī)科學(xué)學(xué)術(shù)會(huì)議ICALP、FSTTCS上發(fā)表多篇重要論文。

相對(duì)于模型檢測(cè)，程序驗(yàn)證是直接針對(duì)程序代碼的，就是研究如何驗(yàn)證程序代碼正確性的方向。在程序驗(yàn)證方面，符鴻飛在程序終止性及運(yùn)行時(shí)間驗(yàn)證方面取得諸多基礎(chǔ)性理論結(jié)果，并發(fā)表在國(guó)際頂級(jí)形式化方法、人工智能及程序語(yǔ)言學(xué)術(shù)會(huì)議POPL、CAV、IJCAI上。首先，他作為主要貢獻(xiàn)者與合作者提出了分級(jí)上鞅在同時(shí)帶有惡意非確定性與友善非確定性概率程序上的定義，并給出了線性分級(jí)上鞅的合成算法以及相關(guān)的計(jì)算復(fù)雜性，進(jìn)而為帶有非確定性的概率程序終止性與期望運(yùn)行時(shí)間驗(yàn)證提供了一個(gè)堅(jiān)實(shí)的理論基礎(chǔ)；同時(shí)，他也證明了分級(jí)上鞅可以導(dǎo)出有限步內(nèi)不終止概率的指數(shù)衰減性。

其次，符鴻飛通過實(shí)代數(shù)幾何中的一些數(shù)學(xué)定理及半正定規(guī)劃給出了概率程序上合成多項(xiàng)式分級(jí)上鞅的一個(gè)高效算法。

再次，他將分級(jí)函數(shù)推廣至非概率遞歸程序，進(jìn)而通過線性規(guī)劃以及實(shí)代數(shù)幾何上的一些定理給出了一個(gè)輸出非概率遞歸程序精確運(yùn)行時(shí)間的驗(yàn)證算法；該算法可以有效地輸出很多經(jīng)典遞歸算法（如歸并排序、最近點(diǎn)對(duì)算法等）的精確非多項(xiàng)式運(yùn)行時(shí)間。

最后，他基于一元遞歸關(guān)系針對(duì)隨機(jī)遞歸算法給出了一個(gè)驗(yàn)證精確期望運(yùn)行時(shí)間的高效算法，該算法可以在線性時(shí)間內(nèi)輸出一個(gè)由隨機(jī)遞歸算法導(dǎo)出的遞歸關(guān)系的精確期望運(yùn)行時(shí)間。截至目前，符鴻飛已在理論計(jì)算機(jī)科學(xué)、形式化方法國(guó)際著名會(huì)議及期刊上發(fā)表論文14篇。

盡管已經(jīng)取得了許多成績(jī)，但他沒有自滿，而是在已經(jīng)取得成果的基礎(chǔ)上不斷展開新的探索。2016年，他參與了一項(xiàng)國(guó)家自然科學(xué)基金重點(diǎn)項(xiàng)目“大規(guī)模概率并發(fā)實(shí)時(shí)系統(tǒng)模型檢驗(yàn)”。該項(xiàng)目的重點(diǎn)在于研究新的理論方法以有效驗(yàn)證兼具隨機(jī)性、并發(fā)性及實(shí)時(shí)性特征的大規(guī)模系統(tǒng)。隨機(jī)性、并發(fā)性及實(shí)時(shí)性都是難以通過直覺或是大規(guī)模測(cè)試保證正確性的復(fù)雜系統(tǒng)性質(zhì)。通過該項(xiàng)目的研究，能夠在為保證大規(guī)模概率并發(fā)實(shí)時(shí)系統(tǒng)關(guān)鍵性質(zhì)方面給出一個(gè)有效的理論框架。

除了自身的科研工作，符鴻飛還積極承擔(dān)學(xué)術(shù)兼職，為理論計(jì)算機(jī)科學(xué)國(guó)際著名學(xué)術(shù)會(huì)議和期刊ICALP、VMCAI、FOSSACS、Information and Computation、Information Processing Letter等審稿30余篇。目前，他在上海交通大學(xué)帶領(lǐng)博士生和碩士生進(jìn)行形式化方法的研究，并教授“程序語(yǔ)言理論”“離散數(shù)學(xué)”等和形式化方法相關(guān)的課程。同時(shí)，他還與博士導(dǎo)師Joost-Pieter Katoen教授、博士后合作導(dǎo)師Krishnendu Chatterjee教授及國(guó)內(nèi)一些著名學(xué)者保持合作關(guān)系，共同推進(jìn)形式化方法的發(fā)展。

尋求應(yīng)用 教學(xué)傳承

毋庸置疑，形式化驗(yàn)證是一個(gè)偏理論的研究方向，但最近幾年，它在工業(yè)界的應(yīng)用越來越多?！熬幾g器的驗(yàn)證、防止黑客入侵、保障云計(jì)算的安全，這些都離不開形式化驗(yàn)證。”符鴻飛對(duì)此如數(shù)家珍。

2016年在羅馬

所謂編譯器，就是將“一種語(yǔ)言（通常為高級(jí)語(yǔ)言）”翻譯為“另一種語(yǔ)言（通常為低級(jí)語(yǔ)言）”的程序，簡(jiǎn)單來說就是把寫好的代碼轉(zhuǎn)化成直接可執(zhí)行的二進(jìn)制文件。編譯器是一個(gè)比較關(guān)鍵的系統(tǒng)軟件，如果它出錯(cuò)的話，那么通過這個(gè)編譯器所編譯的二進(jìn)制的文件都可能有問題，因此，運(yùn)用形式化方法保障其正確性至關(guān)重要。

對(duì)于操作系統(tǒng)而言，防止外部傷害如黑客入侵是必須要考慮的關(guān)鍵點(diǎn)。一般來說，黑客想要入侵操作系統(tǒng)，就必須要攻擊程序員在寫程序的時(shí)候沒有考慮到的漏洞。而通過形式化方法，可以交由計(jì)算機(jī)去檢查漏洞，如果最終通過定理證明的方法證明了操作系統(tǒng)沒有漏洞的話，就可以說這個(gè)操作系統(tǒng)在形式化驗(yàn)證的正確性定義下是安全的?！斑@方面目前已經(jīng)做出了相關(guān)的操作系統(tǒng)，并且成功通過了黑客的攻擊測(cè)試?！?/p>

形式化驗(yàn)證的應(yīng)用還體現(xiàn)在備受矚目的云計(jì)算技術(shù)上。毫無疑問，云計(jì)算是21世紀(jì)到目前為止最成功的技術(shù)之一，對(duì)于任何規(guī)模的企業(yè)都能提供不同程度的幫助。正因?yàn)榇耍ㄟ^形式化方法排除系統(tǒng)的錯(cuò)漏尤為重要。

或許有人會(huì)覺得，理論研究是一項(xiàng)與實(shí)際相距甚遠(yuǎn)的工作，大多是空中樓閣。但符鴻飛不這么想，他堅(jiān)決反對(duì)將理論研究與實(shí)際工作割裂開來。他認(rèn)為，或許某些理論在誕生之初恍若不可實(shí)現(xiàn)，但隨著科學(xué)研究的深入發(fā)展和科學(xué)技術(shù)的不斷進(jìn)步，有朝一日它們或許可以發(fā)揮出各自的作用，甚至直接指導(dǎo)實(shí)踐。正因?yàn)榇?，符鴻飛一直主張從事理論研究的人應(yīng)該對(duì)其所在領(lǐng)域的應(yīng)用情況做一定了解，尤其是計(jì)算機(jī)專業(yè)?！霸谟?jì)算機(jī)專業(yè)從事理論研究與在數(shù)學(xué)、物理等專業(yè)是不一樣的，后者可以做一些很純粹的理論研究，而計(jì)算機(jī)專業(yè)則需要關(guān)注工業(yè)界的發(fā)展，以期早日與實(shí)踐接軌?！彼f。

博士畢業(yè)照

作為青年科學(xué)家，符鴻飛很慶幸選擇了上海交通大學(xué)，加入了John Hopcroft中心和BASICS實(shí)驗(yàn)室。為了加快培育青年學(xué)者，學(xué)校有著良好的學(xué)術(shù)氛圍，讓他能夠心無旁騖地從事科研和教學(xué)工作。

在教學(xué)方面，符鴻飛認(rèn)為要把學(xué)生放在首位。如在設(shè)計(jì)教學(xué)內(nèi)容的時(shí)候，應(yīng)該考慮什么樣的內(nèi)容是對(duì)學(xué)生有幫助的，在進(jìn)行教學(xué)的時(shí)候可以先站在學(xué)生的角度看待問題，設(shè)想學(xué)生會(huì)如何去學(xué)習(xí)新的知識(shí)?！皩W(xué)生在學(xué)習(xí)一門課程前有他們自己的知識(shí)結(jié)構(gòu)，如果教師嚴(yán)格按照自己對(duì)課程內(nèi)容的把握上課，有可能會(huì)導(dǎo)致學(xué)生無法將新的知識(shí)同原有的知識(shí)結(jié)構(gòu)建立起聯(lián)系，因此教師首先要從學(xué)生的角度出發(fā)講課，直到學(xué)生能夠循序漸進(jìn)地掌握課程內(nèi)容?！狈欙w說。同時(shí)，由于學(xué)生的情況各不相同，在掌握課程內(nèi)容方面多有差異，因此教師要對(duì)每個(gè)學(xué)生都有耐心，盡量解決每個(gè)學(xué)生的問題。另外，在教學(xué)的時(shí)候，應(yīng)注意調(diào)動(dòng)學(xué)生的積極性、活躍課堂氣氛。這樣做的好處是學(xué)生的注意力會(huì)一直比較集中，同時(shí)學(xué)生也能夠主動(dòng)參與到課程的學(xué)習(xí)中，提高教學(xué)效果。最后，在課程內(nèi)容的設(shè)置方面要聯(lián)系整個(gè)專業(yè)背景，力求學(xué)生在修習(xí)過課程后能夠更好地適應(yīng)專業(yè)發(fā)展趨勢(shì)。講課時(shí)要注意保持講課邏輯的一致性和內(nèi)在關(guān)聯(lián)性，使得學(xué)生能夠融會(huì)貫通，還要隨時(shí)觀察學(xué)生掌握課程內(nèi)容的情況并進(jìn)行有必要的干預(yù)。

科學(xué)研究最重要的就是傳承，科研成果的取得離不開一代代研究者在繼承的基礎(chǔ)上加以創(chuàng)新。符鴻飛希望通過自己的教學(xué)，盡快培養(yǎng)出具有扎實(shí)專業(yè)背景、能夠自主開展科研工作的學(xué)生，共同探索如何將所創(chuàng)理論應(yīng)用于實(shí)踐。

從事理論研究是一項(xiàng)孤獨(dú)的工作，截至目前，符鴻飛的絕大多數(shù)成果都是自己獨(dú)立完成的。盡管如此，他依然對(duì)這個(gè)研究方向保持著濃厚的興趣。在他看來，研究工作的意義就是他的動(dòng)力?！爸灰氲侥軌蛴米陨硭鶎W(xué)做出貢獻(xiàn)，所有獨(dú)行的孤寂和壓力就都得到了慰藉?！彼f。