中文摘要：

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

结论摘要：

混合系统成为计算机和控制领域科学家共同关注的一个热点问题。经过课题研究，我们建立了混合系统的一个计算模型；基于该模型，建立了一个实时逻辑（TITL）和混合投影时序逻辑（HPTL）系统，它既是系统刻画语言又是系统规范语言。建立了一个可视化的系统刻画语言（HM），并建立了从这个语言到时序逻辑语言的转换规则。建立了时序逻辑语言PTL的模型理论，解决了投影命题时序逻辑PPTL可满足性的判定问题，给出了判定算法。建立了它的一个公理系统。同时，PTL的一个子集被开发成一个可执行语言，基于该语言可以对混合系统进行模拟验证；给出了该语言的模型语义和操作语义。进一步，证明了TITL的可满足性是不可判定的；给出该逻辑的一个可判定子类TITLsub。深入研究了混合系统的子类矩形系统和多速率系统的符号化可达性分析，给出了一个较好的分析算法；证明了多速率系统的可判定性。这些工作，对基于PTL（TITL，HPTL）的混合系统形式验证包括模型检测、演绎、模拟验证等奠定了坚实基础。作为应用实例，着重研究了基于FPGA的可重构SOPC嵌入式系统的建模和分析验证以及对等计算（P2P）和WEB服务的建模、合成和验証。