段振华，男林，博士，教授，博士生导师。1982年来自和1987年分别获西北大学学根心八类士和硕士学位，1989年360百科到英国学习。1996年7月和1997年2月分别获Newcastl础章济e大学理学博士学位和看陈程千阳象Sheffie体英台困许源空课ld大学工学博士学位。
- 中文名称 段振华
- 职称 博士，教授，博士生导师
- 性别 男
- 承担项目 高可信软件技术等
人物简介
2来自003年回国工作。现任西安电子科技大学计算理论与技术研究所所长，校学术振兴计划现代计算首席专家，校可信软件创新团队首席专家，享受政府特殊津贴。
360百科 在国外学习和工作期间，主要从事高可信软件的开发方法和验证技术的研究，参加了英国两项SERC(EPSRC)(相当国家自然科学基金项目)研究课题。发表了20多篇学术论文。他是IEEE高级会员，中国计算机学会高级会员，美国数学评论(Mathem八六天可脚atical Reviews)特邀评论员。国家自然科学基金委第十三届信息科学部专家评审组成员，陕西省学位委员会第三届学科评议组成员。曾担任5个著名国际学术会议程序委员会或组委会主席(TASE 2011，TAMC 2008，ACSD 2008, Petri Nets 2008，CSCWD 2008)，40多个主流国际学术会议程序委员会委员。主持国家973项目子课题，国家自然科学基金重点、重大国际合作、重大研究计划(培育)、以及面上等多项国家项目。
回国工作年来，主要从事高可信软件理论与技术，互联网计算和互联网软春其想统减置果件技术及基于 FPGA的SOPC嵌入式系统的研究。主持国家自然科学基金重点项目"框架时序逻辑程序设计"1项(已完成，优秀)，国家自然科学基金项目(混合系统的形式验证)1项(已完成，优秀)，总装备部的11该识些让报掌需群跑5预言项目1项(采依板通本在研)，国家自然致科学基金国际重大合作项目1项(在研)，973计划项目子课题1项(在研)。 在Theoretical Computer Science, Acta Informatica, Biosystem黑卫资粮供击难成s, Science of Computer Programming, Mathematic极优果助书伤似兰武个距al Structures in Computer Science, 和Journal of Logic and Algebr罗屋热移笑械房积aic 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)
总项目名称:信息服务的模型与机理研究。
研究内容:建立适用于描述网络环境下业务要求的需求模型，提供用户主导、面向领域的业务视图动态获取及演化理论。研究需求模型的验证和确认技术，确保需求的正确性、完整性、一致性和极小冗余性，进而提供有效支持多用户群体的需求协同技术和需求规格逐步优化的策略与方法。
