混成系统设计演算

本项目在研究比较国内外混合系统开发方法的基础上，从混合系统的形式模型和语义、形式验证方法和支撑工具等方面对混合系统的形式化方法开展了研究，主要成果有：提出了一种混合系统模型设计语言及其混合变迁语义，并提出了一个基于三值区间的模型检验算法；利用超密时段演算，以混合通讯顺序进程描述语言为基础，提出混合系统的超密时段语义；提出一种带next算子的时段演算用以推理超密计算下的动作和事件；提出了分布实进概率系统定性和定量验证的模型检验算法；提出了一种基于树自动机的高效模型检验算法；在PVS上设计并实现了一个支持包括时段演算在内的区间逻辑推理的实时系统验证工具；提出了区间逻辑的标记相继式演算；等等。