【人物简介】

　　段振华，博士，教授，博士生导师。1982年和1987年分别获西北大学学士和硕士学位，1989年到英国学习。1996年7月和1997年2月分别获Newcastle大学理学博士学位和Sheffield大学工学博士学位。2003年回国工作。现任西安电子科技大学计算理论与技术研究所所长。

【研究方向】

(1)高可信软件技术 (2)P2P与服务计算(包括云计算) (3)基于FPGA的嵌入式系统

【研究成果】

【科研项目】

　　框架时序逻辑程序设计语言—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月