導師姓名 段振華
導師類型 碩士生導師、博士生導師
工作狀態 在職
職稱 教授
最高學歷 博士研究生

碩士學科
(081202)計算機軟件與理論
博士學科
(081202)計算機軟件與理論

工作單位 計算理論與技術研究所
辦公電話 029-88202883
辦公地址 新科技樓705 通訊地址
電子郵箱 zhenhua_duan@126.com
主頁地址 http://web.xidian.edu.cn/zhhduan/

個人簡歷
段振華，博士，教授，博士生導師。1982年和1987年分別獲西北大學學士和碩士學位，1989年到英國學習。1996年7月和1997年2月分別獲Newcastle大學理學博士學位和Sheffield大學工學博士學位。2003年回國工作?，F任西安電子科技大學計算理論與技術研究所所長。

主要研究方向及感興趣的領域
（1）高可信軟件技術；
（2）P2P與服務計算（包括云計算）；
（3）基于FPGA的嵌入式系統。

研究成果與著作、個人代表作、獲獎情況
段教授領導的團隊，開發了5個與項目相關的軟件系統原型：
● 框架時序邏輯程序設計語言—Framed Tempura 解釋器
● Hp2p 軟件
●模型檢測器原型
●Web Services支持環境
●用c/c++語言設計開發了一個運行于linux操作系統的具有彩色圖形界面的 FPGA支持軟件。

已經發表的與項目相關的論文有：
[1] Zhenhua Duan, Xiaoxiao Yang, Maciej Koutny, Framed Temporal Logic Programming, Science of Computer Programming, Elsevier Science，Accepted paper. 2007
[2] Zhenhua Duan, Cong Tian and Li Zhang, A Decision Procedure for Propositional Projection Temporal Logic with Infinite Models. Acta Informatica. Accepted Paper. 2007
[3] Zhenhua Duan and Maciej Koutny, A framed temporal logic programming language, Journal of Computer Science and Technology, Vol 19, No.3, May 2004
[4] Duan Z., Holcombe M., Bell A., A logic for biological systems. Elsevier Science, BioSystems 55 (2000) 93-105, 2000
[5] Lihui Lei, Zhenhua Duan, Integrating AJAX and Web services for cooperative image editing, IT Professional, Vol9, No 3, p 25-29,May/June, 2007
[6] Zhenhua Duan, Temporal Logic and Temporal Logic Programming. Science Press, China, 2006.
[7] Zhenhua Duan, Modeling and Analysis of Hybrid Systems. Science Press, China, 2005.
[8] Zhenhua Duan, Xiaoxiao Yang, Maciej Koutny, Semantics of Framed Temporal Logic Programs,Proceedings of ICLP2005 Spain, Sigtes, LNCS 3886, pp.356-370, Springer Verlager, Oct. 2005
[9] Zhenhua Duan and Cong Tian, Decidability of Propositional Projection Temporal Logic with Infinite Models. Theory and Applications of Models of Computation, Lecture Notes in Computer Science, 4484, 521-532. Springer-Verlag, 2007
[10] Cong Tian and Zhenhua Duan, Model Checking Propositional Projection Temporal Logic Based on SPIN. ICFEM 2007, Lecture Notes in Computer Science, 4789, 246-265. Springer-Verlag, 2007
[11]Xiaoxiao Yang, Zhenhua Duan, Operational Semantics of Framed Temporal Logic Programs, SOFSEM 2007, LNCS 4362,pp.566-578. Springer Verlag, Jan.2007
[12] Yongtao Ma, Zhenhua Duan, Xiaobing Wang, Xiaoxiao Yang: An Interpreter for Framed Tempura and Its Application. TASE 2007: 251-260，Shanghai, 2007
[13] Peng Men, Zhenhua Duan, Bin Yu, Utilizing Fuzzy Petri Net for Choreagraphy Based Semantic Web Services Discovery, ATPN07,Siedlce, Poland, LNCS, Springer, 6,2007
[14] Lihui Lei , Zhenhua Duan, Semantic Matching of Web Services for Collaborative Business Processes, LNCS 4202，Springer Verlag, 2007
[15] Lihui Lei, Zhenhua Duan, Automating Web Service Composition for Collaborative Business Processes, CSCWD 07, IEEE, Melbourne,Australia,2007
[16] Zhenhua Duan, Xiaobing Wang, Implementing Pointer in Temporal Logic Programming Languages, Proceeding of SBMF2006, pp.171-184, Natal, Brazil, Sep. 2006
[17] Lihui Lei, Zhenhua Duan, Bin Yu, Semantic Matching of Web Services Based on Choreographies, The Proceedings of the 10th International Conference of Computer Supported Cooperative Work in Design (IEEE), P751-756, Nanjing, China. May 2006
[18]Lihui Lei, Zhenhua Duan, Transforming OWL-S Process Model i n t o EDFA for Service Discovery, The Proceeding of the IEEE International Conference on Web Services (ICWS06), p137-144, Chicago, USA. September, 2006
[19]Zhile Zou, Zhenhua Duan, Jianli Wang, A Comprehensive Framework for Dynamic Web Services Integration, The Proceedings of the 4th IEEE European Conference on Web Services (ECOWS06), p211-220, Zurich, Switzerland, Dec. 2006
[20]Zhile Zou, Zhenhua Duan, Building Business Processes or Assembling Service Components: Reuse Services with BPEL4WS and SCA, The Proceedings of the 4th IEEE European Conference on Web Services (ECOWS06), p138-147, Zurich, Switzerland, Dec. 2006
[21]Duan Z., Koutny M., and Holt C.: Projection in temporal logic programming. In F. Pfenning, editor, Proceeding of Logic Programming and Automatic Reasoning, Lecture Notes in Artificial Intelligence, a subseries of LNCS, Vol.822, pp333-344, Springer Verlag, July, 1994.
[22]Zhuo Peng, Zhenhua Duan, Jian-Jun Qi, Yang Cao, Ertao Lv，“HP2P: A Hybrid Hierarchical P2P Network”,The Proceedings of The First International Conference on the Digital Society (IEEE)(ICDS 2007), Guadeloupe, French Caribbean, Jan. 2007 9．
[23]Ertao Lv, zhenhua Duan, Jian-Jun Qi, Yang Cao and Zhuo Peng,“Incorporating Clusters i n t o Hybrid P2P Network”, The Proceedings of The First International Conference on the Digital Society (IEEE)(ICDS 2007),Guadeloupe, French Caribbean, Jan. 2007
[24] W. Wang and Z. Duan: A Multi-Fingerprints Based AntiSpam Peer-to-Peer Network, ISBN：4-916227-17-4, ISFST’04, Xian, China Oct. 2004
[25]段振華，帶ε的回溯自動機， 計算機科學，8，2003
[26] 雷麗琿 , 段振華，基于工作流模式的OWL-S過程模型分析及其應用，計算機科學，6月 2007
[27] 張海賓，段振華，“多速率混合系統的符號化可達性分析”，西安交通大學學報2007年第四期
[28] 張海賓，段振華，“稠密時間區間時序邏輯的可滿足性判定”， 西安電子科技大學學報 2007年第3期
[29] 張海賓，段振華，“混合投影時序邏輯與混合系統的形式化驗證”，計算機科學 (已錄取)
[30] 劉洪燕，段振華，張鵬飛，“Web服務提供方安全模型的設計、建模和分析”，計算機技術與發展, Vol16, No11, p162-165, 2006
[31] 張海賓*，段振華，“稠密時間區間時序邏輯的可滿足性判定”，西安電子科技大學學報，Vol.34(3):463-467,2007.
[32] 雷麗暉*，段振華，“使用擴展區間時序邏輯為并發工作流建模”，西安電子科技大學學報，Vol.34(4):673-680,2007.
[33] 雷麗暉，段振華，“基于擴展投影時序邏輯的組合Web服務描述與驗證”，西安交通大學學報，2007年第10期 頁碼: 1155-1159
[34]張鵬飛 段振華 田聰“狀態圖到PTL 形式規范的轉化”, 第三屆全國軟件與應用學術會議論文集(《計算機工程與科學》，vol28， No A2, p122-125，Sep.2006
[35] 施小祥，段振華，“劃分和時延驅動的動態可重構FPGA在線布局算法”， 全國第六屆嵌入式系統學術年會論文集《計算機技術與發展》Vol16, 10月, 2006）, 12－15頁,西安, 2006年10月

目前承擔的科研項目及教學情況 目前承擔的項目：
●*****開發方法及支持環境
●信息服務的需求獲取與建模
●構造可信、高效軟件系統的基礎研究
●組合Web服務的建模與驗證
●基于命題投影時序邏輯的模型檢測

目前承擔研究生教學任務：
基于互聯網的計算

如果發現導師信息存在錯誤或者偏差，歡迎隨時與我們聯系，以便進行更新完善。 聯系方式