混合系统的形式验证

建立混合系统的计算模型；基于这个模型，建立一个时序逻辑系统，它既是系统刻画语言又是系统规范语言。建立一个可视化的系统刻画语言，并建立从这个语言到时序逻辑语言的转换规则；建立时序逻辑语言的模型理论，检验可满足性的判定，探索可判定子类的分类，发展该时序逻辑的算法验证方法，包括模型检查。建立该时序逻辑的证明系统，发展基于该系统的演绎法对混合系统进行形式验证的规则和方法。建立一个层次的刻画语言，用以在不同抽象级上表达混合系统，并逐步求精得到系统的描述。由于HM和HPTL是基础，该研究是源头性的，它具有很重要的意义。