信息物理系统广泛应用于安全攸关领域,因此要保证其正确性与安全性至关重要。混成自动机是一种既包含了离散的状态转移,又存在连续变量变化的形式化建模语言。其中离散的逻辑跳转与连续的变量变化混合的特性使得其可以用于对信息物理系统建模与验证。然而正因为离散跳转与连续行为的交织,使得其状态空间极为复杂,即便是对混成自动机安全性问题的可达性问题的验证也异常困难。在实际的信息物理系统中,由于不同组件通信协作行为的大量存在,组合混成自动机才能满足其建模需求。组合混成自动机由多个单一混成自动机通过同步行为协作构成,其行为比单一混成自动机更为复杂。目前的研究工作能解决的组合混成自动机验证问题的规模极为有限。因此如何提高组合混成自动机可达性验证规模,提升验证效率是十分值得关注与研究的课题。本文针对组合混成自动机的子类——组合线性混成自动机的可达性验证进行了系统化研究,研究内容包括:1.基于混合语义的组合线性混成自动机有界可达性验证。本文工作提出了一种基于混合语义的组合线性混成自动机有界可达性验证方法。该方法采用传统交替语义枚举候选路径,浅同步语义验证路径行为。通过将组合自动机的离散图结构编码为SAT问题的方式寻路,接下来通过将候选路径行为编码为线性约束问题求解的方式来验证路径的可达性。为了更进一步地缩减状态空间,约减遍历的路径数,本文给出了在浅同步语义下一致,而在传统交替语义下不同的三种非典型路径的定义,同时给出了在路径遍历阶段规避非典型路径的编码方法。2.基于多重IIS的组合线性混成自动机面向路径可达性验证加速。IIS加速技术可以用于加速对组合线性混成自动机验证的加速。然而,不同的IIS路径对于路径的约减能力大相径庭。为了利用IIS加速技术约减更多的路径,本文提出了一种基于共享事件分割的多重IIS加速技术。该方法在IIS获取阶段采用多重IIS技术,从一个不可解的约束集提取出多个IIS路径组。接下来,为了将提取的IIS路径锁定在更精确的范围内,提出了一种基于共享事件分割的IIS定位方法。根据共享事件的位置分割路径,在不同的子路径上进一步求解IIS。我们实现了该方法并在业内广泛使用的例子上进行了实验。实验结果表明,采用这一系列的优化后验证效率与处理问题的规模得到了极大的提升,表现优于领域内相关工具。3.基于组合不可行路径的组合线性混成自动机全局性质推导。上述方法在组合线性混成自动机的有界可达性验证上取得了一定的进展,但实际应用中往往需要验证系统的全局性质。因此本文提出了一种基于组合不可行路径的组合线性混成自动机全局性质推导方法。该方法设计了一种针对组合不可行路径的LTL约束编码方式,同时提出了一种非典型路径规避规则的LTL约束编码方法。但这样生成的LTL逻辑约束尤其冗杂,即便是一个只有3,4个自动机的组合系统,生成的LTL逻辑约束也超过了求解器的求解范围。针对这一问题,本文提出了一种LTL约束本地化的方法,极大地缩减了LTL约束,扩展了全局验证的问题规模。当系统模型满足该方法提出的这一形式的LTL规约时,我们的方法可以给出全局证明,并且在许多公认案例上,能以较小的开销得到全局结果。