目前承担的项目：

●

●信息服务的需求获取与建模

●构造可信、高效软件系统的基础研究

●组合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）

总项目名称：信息服务的模型与机理研究。

研究内容：建立适用于描述网络环境下业务要求的需求模型，提供用户主导、面向领域的业务视图动态获取及演化理论。研究需求模型的验证和确认技术，确保需求的正确性、完整性、一致性和极小冗余性，进而提供有效支持多用户群体的需求协同技术和需求规格逐步优化的策略与方法。