在形式化方法領域“攻深探盲”
——記上海交通大學計算機科學與工程系特別副研究員符鴻飛

文/肖延勝

時至今日，上海交通大學特別副研究員符鴻飛在“形式化方法”這一研究領域已經堅守了約10年時間。令他感到欣慰的是，形式化方法研究和應用近年發展非常迅速。10年的攻堅克難與執著創新，也讓他在形式化方法中的兩個重要方向——模型檢測和程序驗證中都取得了一系列的創新成果。

興趣為燈，十年磨一劍

1984年10月，符鴻飛生于上海。出于對與數學關聯緊密的計算機科學的興趣，2003年上大學時他選擇了上海交通大學計算機科學與技術專業。在做計算機編程的過程中，他對如何保證程序編寫的正確性產生了困惑，并進行了初步探索。這為其后來開展形式化方法研究，埋下了伏筆。

2007年本科畢業后，留校攻讀碩士學位的符鴻飛，在導師傅育熙教授的指導下做研究，在互模擬判定及模型檢測算法方面做出了新貢獻。他對利用數學方法證明系統正確性的形式化方法研究的興趣，也正是萌生于這段時間。

畢業后獲得國家公派留學機會，他便選擇了德國亞琛工業大學，師從形式化方法研究領域著名學者Joost-Pieter Katoen教授。亞琛工業大學成立于1870年，被譽為“歐洲的麻省理工”。從2010年到2014年，符鴻飛在這里度過了4年時光，主要的研究方向即為概率系統形式化驗證，通過努力他取得了多項獨創性成果。

符鴻飛特別副研究員2017年參加CAV國際會議

在德國留學期間，符鴻飛的研究興趣和研究視野逐漸走向了理論與應用相結合。由此博士后階段他選擇了理論和應用并重的程序驗證（針對程序的形式化驗證）作為自己的研究方向，并通過與奧地利科學家的合作研究，發表了一系列的研究成果。

縱觀符鴻飛這一段的學習和研究歷程，興趣始終是指引他前行的燈塔，并給了他無盡的前行動力。

創新為帆，碩果滿枝頭

形式化方法如今已在數學、計算機科學、人工智能等領域得到廣泛運用。

作為理論計算機科學的一個分支的形式化方法，簡單來說，就是利用數學和邏輯方法證明計算機系統的正確性，以此為基礎，來驗證、提升系統的可靠性、穩定性、安全性等。

計算機系統中存在潛在漏洞，可能導致重大的人身或財產損失，形式化方法能精確地揭示各種邏輯規律，制定相應的邏輯規則，使各種理論體系更加嚴密，作為一種手段可以幫助推理和證明計算機系統的關鍵系統組件的正確性，提前發現潛在漏洞，并幫助對系統做出改進。

十年磨一劍。秉承創新思維，符鴻飛經過多年埋頭耕耘，主要在形式化方法的模型檢測和程序驗證兩個方向的研究中取得了突破。顧名思義，模型檢測即驗證系統模型正確性的研究，程序驗證是驗證程序正確性的研究。

多年來在模型檢測研究方面，符鴻飛以獨立作者身份給出了關于連續時間馬爾可夫過程時序邏輯的兩個基礎模型檢測算法；著力研究了離散時間馬爾可夫過程上關于互模擬等價關系的可判定性和計算復雜性。在程序驗證方面，他針對概率程序終止性驗證問題提出了分級上鞅在同時帶有惡意與友善非確性概率程序上的定義，并給出了線性分級上鞅的合成算法以及相關的計算復雜性；給出了一個概率程序上合成多項式分級上鞅的高效算法；針對概率程序的資源消耗，給出了一個基礎驗證算法；還給出了一個輸出非概率遞歸程序精確運行時間的驗證算法，相關的研究成果集結成15篇論文，在國際著名會議及期刊上發表，并獲得了HSCC 2013最佳學生論文獎。

十八大以來創新驅動發展戰略大力實施，創新發展理念如今已深入人心。扎根形式化方法研究領域，結合這一研究的特點，符鴻飛對創新有了自己的體會。在他看來，這一研究領域的創新大致有三種形式：（1）通過復雜的數學方法解決一個已經被提出的公認難題；（2）提出新的理論概念，并充分證明其具有理論或實際意義；（3）將理論結果應用到大規模工業系統中，以驗證實際系統中的一些關鍵性質，也是一種創新渠道。

另外他還補充道，現在的創新呈現出一個突出的新特點，即單一要素很難完成，往往需要多要素結合來共同促成創新。創新對學科交叉型團隊的需求越來越明顯，需要在實驗室、生產實踐中對理論進行驗證，這都需要時間，國內外同行之間的交流也變得越來越必要。

志在應用，盼成果落地

除了科研，符鴻飛目前還承擔了教學任務，主講《離散數學》《程序語言理論》等與形式化方法相關的課程。他表示，教學事關傳承，與科研一樣重要。

他是中國計算機學會（CCF）形式化方法專委會通訊委員，曾為諸多國際著名學術會議和期刊擔任審稿工作，承擔過1項“關于大規模并發實時系統模型檢驗”的國家自然科學基金重點項目，該項目的目的是研究開發出新的理論方法，以滿足對兼具隨機性、并發性以及實時性特征的大規模系統的有效驗證。目前他正主持1項國家自然科學青年基金項目。

注重學術交流與合作研究的符鴻飛與他在德國、奧地利深造時的導師均長期保持著合作關系；在國內也與上海交通大學、華東師范大學、中國科學院軟件研究所以及北京大學等機構中致力于形式化方法研究的同行學者，有著密切的交流合作。

科研成果的產業化應用是實現其最大價值的“最后一公里”，雖然形式化方法研究的基礎研究色彩較重，但符鴻飛非常注重結合實際需要來展開研究，也渴望自己的研究成果盡快被產業化應用。

當前形式化方法已經取得了真正的進展，正在被人們用來解決軟件開發中一直沒有解決的問題，也實際開發出了一些重要的系統或系統部件。法國巴黎地鐵14號線的自動駕駛系統就是用形式化方法開發并驗證的，1998年投入運行，至今未發現任何缺陷。

目前符鴻飛正牽手合作單位繼續推進概率程序的終止性驗證、概率程序的資源消耗驗證、概率程序的靈敏性驗證等相關工作。他期望這些工作能盡快圓滿完成，并得到學術界認可。

“我更期待著不久的將來自己的研究成果能在工業界關鍵場合獲得應用?！狈欙w說。