混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,针对混成系统的形式化建模与验证是确保其正确性和可靠性的重要途径。混成系统不仅含有复杂的动态行为、时间限制,还包括与外部环境的通信等特征,针对混成系统的形式化规范技术必须能够描述所有这些方面,但是单一的规范技术很难适合这样的应用场景。在具体分析和验证混成系统时,由于混成系统状态空间是无限的,关于混成系统的诸多研究问题(可达性问题、模型检测等)都是不可判定的。本文主要包括如下四个方面的研究工作。(1)本文基于描述系统行为各个方面这一想法,首先组合了三种已经被广泛研究的规范技术:接口自动机、多速率混成自动机和Z语言,称为多速率混成ZIA规范,该规范不仅可以描述多速率混成系统软件组件接口性质、混成时序性质,还具有很强的描述数据性质的能力。(2)本文给出了连续时间ZIA规范上的互模拟关系定义,不仅考虑行为间的互模拟关系,还考虑了数据间的互模拟关系;然后,基于有限论域CT-ZIA规范,给出了其上的互模拟检测算法,并对算法正确性进行了说明。(3)本文提出了针对多速率混成ZIA规范(MZIA)的带数据约束时序逻辑,考虑到实际应用中对混成系统中连续变量的测量存在误差,该逻辑可以刻画MZIA规范“近似满足”满足某个给定的系统性质;接下来,提出了针对多速率混成系统的一种近似模型检测算法,用来判定一个MZIA规范描述的系统是否近似满足某个带数据约束的时序逻辑公式描述的性质;最后,通过对锅炉系统的例子详细展示了MZIA规范的建模过程以及其上的近似模型检测步骤,说明了本文方法是可行和有效的。(4)本文给出了多速率混成ZIA规范上的精化关系的定义,这种精化关系不仅考虑了动作行为的“交替模拟”,还包含了数据间的精化关系;然后,提出了针对有限论域MZIA规范的精化检测算法,该算法可以自动验证系统的规范到实现的正确性;最后,基于锅炉系统实例展示了精化检测的具体过程。