基本信息
段振华　教授
硕导/博导
博士学科：(081203)计算机应用技术
硕士学科：(081202)计算机软件与理论
工作单位：计算机学院

联系方式
通信地址：
电子邮箱：zhenhua_duan@126.com
办公电话：
办公地点：新科技楼705


个人简介
段振华，博士，教授，博士生导师。分别于1982年和1987年在西北大学获得计算机科学学士和软件工程硕士学位，1989年赴英国留学，1996年、1997年先后获得英国Newcastle大学理学博士和Sheffield大学工学博士学位，并在Sheffield大学从事博士后研究一年。
先后在英国、美国、德国和法国的多个著名公司任软件工程师，从事软件系统的研制和开发.
2003年元月回国至今在西安电子科技大学工作。
现任西安电子科技大学计算理论与技术研究所所长，校学术振兴计划现代计算首席专家，校可信软件创新团队首席专家，享受政府特殊津贴。
个人主页：http://cs.xidian.edu.cn/ds/dslist.asp?showApply=90
人物特写：http://www.xde6.net/view-19677.html



主要研究方向
1.并发、实时、混合系统的理论和应用技术
2.基于Internet和Web服务的软件设计，开发和计算技术（包括中间件，构件，XML，语义WEB，网格和P2P）
3.可编程芯片（PLD和FPGA）的支持软件技术

---

基本信息
段振华　教授
硕导/博导
博士学科：(081203)计算机应用技术
硕士学科：(081202)计算机软件与理论
工作单位：计算机学院

联系方式
通信地址：
电子邮箱：zhenhua_duan@126.com
办公电话：
办公地点：新科技楼705


个人简介
段振华，博士，教授，博士生导师。分别于1982年和1987年在西北大学获得计算机科学学士和软件工程硕士学位，1989年赴英国留学，1996年、1997年先后获得英国Newcastle大学理学博士和Sheffield大学工学博士学位，并在Sheffield大学从事博士后研究一年。
先后在英国、美国、德国和法国的多个著名公司任软件工程师，从事软件系统的研制和开发.
2003年元月回国至今在西安电子科技大学工作。
现任西安电子科技大学计算理论与技术研究所所长，校学术振兴计划现代计算首席专家，校可信软件创新团队首席专家，享受政府特殊津贴。
个人主页：http://cs.xidian.edu.cn/ds/dslist.asp?showApply=90
人物特写：http://www.xde6.net/view-19677.html



主要研究方向
1.并发、实时、混合系统的理论和应用技术
2.基于Internet和Web服务的软件设计，开发和计算技术（包括中间件，构件，XML，语义WEB，网格和P2P）
3.可编程芯片（PLD和FPGA）的支持软件技术

---

科学研究
目前承担的项目：
●
●信息服务的需求获取与建模
●构造可信、高效软件系统的基础研究
●组合Web服务的建模与验证
●基于命题投影时序逻辑的模型检测
段教授领导的团队，开发了5个与项目相关的软件系统原型： ● 框架时序逻辑程序设计语言―Framed Tempura 解释器 ● Hp2p 软件 ●模型检测器原型 ●Web Services支持环境 ●用c/c++语言设计开发了一个运行于linux操作系统的具有彩色图形界面的 FPGA支持软件。
主持国家自然科学基金重点项目“框架时序逻辑程序设计”1项(已完成，优秀)，国家自然科学基金项目（混合系统的形式验证）1项（已完成，优秀），总装备部的115预言项目1项（在研），国家自然科学基金国际重大合作项目1项（在研），*科研项目*子课题1项（在研）。
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、信息服务的需求获取与建模（*科研项目*子课题,2010.1-2014.8）
总项目名称：信息服务的模型与机理研究。
研究内容：建立适用于描述网络环境下业务要求的需求模型，提供用户主导、面向领域的业务视图动态获取及演化理论。研究需求模型的验证和确认技术，确保需求的正确性、完整性、一致性和极小冗余性，进而提供有效支持多用户群体的需求协同技术和需求规格逐步优化的策略与方法。

---

学术论文
发表了20多篇学术论文和研究报告.
已经发表的与项目相关的论文有：
[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月

---

荣誉获奖
获电子工业部科技进步二等奖1项、陕西省科技进步三等奖1项、石油部石油天然气总公司科技进步三等奖1项；
发表学术论文20多篇，出版研究专著一部。
近年来，在国际杂志、会议和国内杂志上发表了60多篇与项目相关的论文。

---

科研团队
团队教师




博士研究生
硕士研究生

---

课程教学
目前承担研究生教学任务：基于互联网的计算

---

招生要求
~~~~~~~~~~~~~~~~~~~~~~~~~~
关于研究生招生的信息：
~~~~~~~~~~~~~~~~~~~~~~~~~~
2010年预计招收硕士研究生10-12名，博士研究生5名