微分半代数程序模型的等价及等价谱系

行为等价是软件程序设计与验证分析的基础。微分半代数混杂系统是近年来出现的新型形式化程序刻画模型，在工程技术领域具有极其广泛的应用。针对微分半代数程序模型，目前较为完善的等价理论还没有建立起来。本项目通过并发理论、微分代数符号计算以及符号与数值混合计算方法的交叉、融合与应用研究，采用带微分半代数方程组状态转移标记的混杂变迁系统，系统地构建微分半代数程序模型的行为等价理论。具体包括，（1）等价的定义：基于微分半代数程序模型的各类动态行为特征，建立模型的线性与分支时间等价以及相应的带误差的近似等价关系；（2）等价的判定：研究微分半代数程序模型各类等价关系的可判定性，并实现带误差但误差可控的近似等价计算方法；（3）等价间的关系：通过等价概念之间粗糙程度的比较关系，构建微分半代数程序模型的等价谱系。在实证示范和实际应用方面，探索在轨道高速列车运行控制软件系统设计与验证分析中的应用。

微分半代数混杂系统是近年来出现的一种刻画程序的形式化模型，在工程技术领域内具有极其广泛的应用。在软件程序设计与验证分析方面，行为等价和等价谱系研究是一项重要的基础工作。本项目通过并发理论、微分半代数符号计算以及符号与数值混合计算方法的交叉、融合，采用带微分半代数方程组状态迁移标记的混杂变迁系统，系统地构建了微分半代数程序模型的行为等价理论，构建了包含不同粗糙程度行为等价的等价谱系。项目解决或部分解决了以下几个问题：（1） 等价的定义：基于微分半代数程序模型的各类动态行为特征，建立了模型的线性与分支时间等价以及相应的带误差的近似等价关系；（2） 等价的判定：利用微分半代数符号计算以及符号与数值混合计算的方法，研究了微分半代数程序模型的各类等价关系的可判定性问题，并合理地实现了部分带误差但误差可控的近似等价计算方法；（3） 等价间的关系：通过比较各等价概念之间的粗糙程度，构建了微分半代数程序模型的等价谱系；（4） 行为性质的保持：通过构建微分半代数程序模型的逻辑推理系统，研究了若干重要行为性质在各等价关系下的保持情况。在实证示例和实际应用方面，探索微分半代数程序模型在列车运行控制系统设计与验证分析以及集成电路设计验证中的应用。已发表或录用论文33篇，出版著作1本，组织了一场国际会议。