![段振華[西安電子科技大學計算理論與技術研究所所長]](/img/0/318/nBnauM3X4MzM0YTNxUDN2YTM1UTM1QDN5MjM5ADMwAjMwUzL1QzL0AzLt92YucmbvRWdo5Cd0FmLwE2LvoDc0RHa.jpg "段振華[西安電子科技大學計算理論與技術研究所所長]")
人物簡介
2003年回國工作。現任西安電子科技大學計算理論與技術研究所所長，校學術振興計畫現代計算首席專家，校可信軟體創新團隊首席專家，享受政府特殊津貼。
在國外學習和工作期間，主要從事高可信軟體的開發方法和驗證技術的研究，參加了英國兩項SERC（EPSRC）（相當國家自然科學基金項目）研究課題。發表了20多篇學術論文。他是IEEE高級會員，中國計算機學會高級會員，美國數學評論（Mathematical Reviews）特邀評論員。國家自然科學基金委第十三屆信息科學部專家評審組成員，陝西省學位委員會第三屆學科評議組成員。曾擔任5個著名國際學術會議程式委員會或組委會主席（TASE 2011，TAMC 2008，ACSD 2008, Petri Nets 2008，CSCWD 2008），40多個主流國際學術會議程式委員會委員。主持國家973項目子課題，國家自然科學基金重點、重大國際合作、重大研究計畫（培育）、以及面上等多項國家項目。
回國工作年來，主要從事高可信軟體理論與技術，網際網路計算和網際網路軟體技術及基於 FPGA的SOPC嵌入式系統的研究。主持國家自然科學基金重點項目“框架時序邏輯程式設計”1項(已完成，優秀)，國家自然科學基金項目（混合系統的形式驗證）1項（已完成，優秀），總裝備部的115預言項目1項（在研），國家自然科學基金國際重大合作項目1項（在研），973計畫項目子課題1項（在研）。 在Theoretical Computer Science, Acta Informatica, Biosystems, Science of Computer Programming, Mathematical Structures in Computer Science, 和Journal of Logic and Algebraic Programming等著名國際期刊和國際會議上發表論文100餘篇。主要研究方向包括：高可信軟體技術，網際網路計算技術，以及嵌入式軟體技術。
承擔項目
1、高可信軟體技術（十一五預研項目）
該項目目標是建立面向構件和服務、模型驅動的高可信軟體開發方法、工具和環境。該方法以模型驅動為核心，以生成面向構件和服務的軟體體系為目的，以模型檢測驗證技術，測試技術和模擬技術為高可信保障。同時，該方法支持高效獲取需求，需求驗證和確認。給出該方法的過程模型，圍繞該模型，開發包括轉換工具，驗證工具，測試工具和模擬工具在內的支持環境。
2、框架時序邏輯程式設計（國家自然科學基金重點項目）
該項目目標是定義框架時序邏輯的語法和語義，建立該邏輯系統的模型理論，公理系統；基於該邏輯系統，開發一個簡潔、實用的、具有類似於C,C++ 和Java語言的程式設計風格的時序邏輯程式設計語言。該語言能支持結構化程式設計、部分面向對象和面向構件程式設計。研究該語言的操作語義和公理語義。開發該語言的一個解釋器。研究該語言在並發、實時和混合系統中的套用。研究架構時序邏輯在網際網路計算及嵌入式系統中的套用。
該研究對提高軟體系統的形式驗證的自動化程度、提高軟體的可靠性和安全性具有積極的促進作用。框架時序邏輯程式設計的研究是源頭性的，具有十分重要的理論意義和廣闊的套用前景。已結題，答辯成績為優。
3、混合系統形式驗證（國家自然科學基金面上項目）
該項目要建立混合系統的計算模型；基於這個模型，建立一個時序邏輯系統，它既是系統刻畫語言又是系統規範語言。建立一個可視化的系統刻畫語言，並建立從這個語言到時序邏輯語言的轉換規則；建立時序邏輯語言的模型理論，檢驗可滿足性的判定，探索可判定子類的分類，發展該時序邏輯的算法驗證方法，包括模型檢查。建立該時序邏輯的證明系統，發展基於該系統的演繹法對混合系統進行形式驗證的規則和方法。建立一個層次的刻畫語言，用以在不同抽象級上表達混合系統，並逐步求精得到系統的描述。
4、混合系統的模型檢查及支持工具（博士學科基金重點項目）
該項目的研究內容是兩方面的，從理論上，要建立一個時序邏輯的模型理論，檢驗它的可滿足性的判定問題，劃分它的可判定子類，建立有效的模型檢查算法。在套用上，要開發一個支持模型檢查的工具，利用該工具對混合系統進行形式驗證。因此，該項目的研究可以減小混合系統驗證的難度，提高混合系統驗證的效率。
5. 組合Web服務的建模與驗證（國家自然科學基金面上項目，2009.1-2011.12）
以投影時序邏輯的可執行子集Framed Tempura 為基礎，定義組合Web 服務建模語言WS-Tempura 的語句結構和通信機制，研究該語言的操作語義，並開發該語言的解釋器。研究該語言的正則形及正則圖，研究該語言的可判定性，判定算法及算法複雜度。研究BPEL 流程到WS-Tempura 程式的轉換規則，並開發自動轉換工具，以實現BPEL 流程模型的自動提取。研究基於WS-Tempura 程式執行的仿真和錯誤診斷技術；基於執行生成的正則圖，研究該圖的性質以及相關的程式分析技術。以WS-Tempura 建模語言描述組合Web 服務的行為，以PPTL 描述組合Web 服務的性質，研究基於模型檢測工具SPIN 的驗證方法；同時，在由WS-Tempura 和PPTL 組成的統一時序邏輯框架下，研究基於SAT 的模型、性質一體化的組合Web 服務驗證方法。
6、構造可信、高效軟體系統的基礎研究（國家自然科學基金國際重大合作項目，2010.1-2012.12）
研究內容：以投影時序邏輯（PTL）、Petri 網和SOFL 為基礎，採用驗證、測試和模擬分析相結合的方法，研究構造可信、高效軟體系統的理論和方法。擴展PTL 的可執行子集MSVL，使之具有描述異步通信的功能，並研究基於MSVL 的模型檢測、定理證明以及模擬分析等驗證理論和方法；研究基於PPTL 的符號、限界、偏序和組合模型檢測，以減少狀態空間；擴展Petri網和進程代數，建立一個新模型，該模型能夠支持進程動態產生/銷毀、通信連線和重構；研究基於該模型的模擬、unfold分析及模型檢測理論和方法；在SOFL 語言的基礎上，研究模型檢測與基於模型的測試相結合的驗證理論和方法；套用上述理論和方法對嵌入式系統和網路軟體進行建模、測試、模擬分析和驗證。
7、信息服務的需求獲取與建模（973計畫項目子課題,2010.1-2014.8）
總項目名稱：信息服務的模型與機理研究。
研究內容：建立適用於描述網路環境下業務要求的需求模型，提供用戶主導、面向領域的業務視圖動態獲取及演化理論。研究需求模型的驗證和確認技術，確保需求的正確性、完整性、一致性和極小冗餘性，進而提供有效支持多用戶群體的需求協同技術和需求規格逐步最佳化的策略與方法。
