導(dǎo)師姓名 段振華
導(dǎo)師類型 碩士生導(dǎo)師、博士生導(dǎo)師
工作狀態(tài) 在職
職稱 教授
最高學(xué)歷 博士研究生

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

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

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

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

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

已經(jīng)發(fā)表的與項目相關(guān)的論文有：
[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]段振華，帶ε的回溯自動機， 計算機科學(xué)，8，2003
[26] 雷麗琿 , 段振華，基于工作流模式的OWL-S過程模型分析及其應(yīng)用，計算機科學(xué)，6月 2007
[27] 張海賓，段振華，“多速率混合系統(tǒng)的符號化可達性分析”，西安交通大學(xué)學(xué)報2007年第四期
[28] 張海賓，段振華，“稠密時間區(qū)間時序邏輯的可滿足性判定”， 西安電子科技大學(xué)學(xué)報 2007年第3期
[29] 張海賓，段振華，“混合投影時序邏輯與混合系統(tǒng)的形式化驗證”，計算機科學(xué) (已錄取)
[30] 劉洪燕，段振華，張鵬飛，“Web服務(wù)提供方安全模型的設(shè)計、建模和分析”，計算機技術(shù)與發(fā)展, Vol16, No11, p162-165, 2006
[31] 張海賓*，段振華，“稠密時間區(qū)間時序邏輯的可滿足性判定”，西安電子科技大學(xué)學(xué)報，Vol.34(3):463-467,2007.
[32] 雷麗暉*，段振華，“使用擴展區(qū)間時序邏輯為并發(fā)工作流建?！保靼搽娮涌萍即髮W(xué)學(xué)報，Vol.34(4):673-680,2007.
[33] 雷麗暉，段振華，“基于擴展投影時序邏輯的組合Web服務(wù)描述與驗證”，西安交通大學(xué)學(xué)報，2007年第10期 頁碼: 1155-1159
[34]張鵬飛 段振華 田聰“狀態(tài)圖到PTL 形式規(guī)范的轉(zhuǎn)化”, 第三屆全國軟件與應(yīng)用學(xué)術(shù)會議論文集(《計算機工程與科學(xué)》，vol28， No A2, p122-125，Sep.2006
[35] 施小祥，段振華，“劃分和時延驅(qū)動的動態(tài)可重構(gòu)FPGA在線布局算法”， 全國第六屆嵌入式系統(tǒng)學(xué)術(shù)年會論文集《計算機技術(shù)與發(fā)展》Vol16, 10月, 2006）, 12－15頁,西安, 2006年10月

目前承擔(dān)的科研項目及教學(xué)情況 目前承擔(dān)的項目：
●*****開發(fā)方法及支持環(huán)境
●信息服務(wù)的需求獲取與建模
●構(gòu)造可信、高效軟件系統(tǒng)的基礎(chǔ)研究
●組合Web服務(wù)的建模與驗證
●基于命題投影時序邏輯的模型檢測

目前承擔(dān)研究生教學(xué)任務(wù)：
基于互聯(lián)網(wǎng)的計算

如果發(fā)現(xiàn)導(dǎo)師信息存在錯誤或者偏差，歡迎隨時與我們聯(lián)系，以便進行更新完善。 聯(lián)系方式