混成系统是一类包含连续和离散行为的复杂系统,被广泛应用于工业控制系统的建模,混成自动机是当前其主流建模语言,混成自动机的有界模型检验是保障系统可靠性和安全性的重要途径。混成自动机有界模型检验的基本思想是通过SMT (Satisfiability Modulo Theories)技术对系统在阈值内的行为进行编码并求解,以检验系统是否满足相关性质。但是由于这种方法需要提前一次性计算出系统阂值内所有的状态空间,如此高的计算复杂性限制了其能处理的系统规模,难以应用到工业界的实际系统。另一种解决问题的思路是将整个系统的有界模型检验问题分解成系统内各路径的检验问题来控制单次验证的复杂度,在此基础上遍历系统内路径完成整个系统的有界模型检验。尽管这种面向路径的有界模型检验途径有效地提升了可检验的系统规模,但是当面对工业界的大规模系统时仍然需要有效的优化技术进一步控制解决问题的复杂性。本文基于混成系统面向路径的有界模型检验途径,针对有界可达性问题研究相关优化技术,在状态空间约减、组合系统遍历优化、基于局部验证推导全局性质、非线性系统检验等四个方面取得以下结果：·提出了SAT-HS-LP联合反馈制导的状态空间约减方法。首先基于SAT编码模型的离散结构有向图并求解,尽量在早期发现不可行路径；然后针对在路径可达性检验过程中确定的不可行路径,利用不可约不可解子集(Irreducible Infeasible Subset, IIS)技术从中定位出不可行子路径片段,在后续的搜索中只需枚举不包含相关不可行路径片段的路径进行检验,从而约减了状态空间。实验显示,该方法大幅度地提升了面向路径有界可达性检验的性能和规模。·针对组合线性混成系统,提出了一种基于组合IIS路径抽取的遍历优化方法。基于SMT编码模型的离散结构有向图并求解,从而在组合系统的图结构上快速枚举出符合同步语义的路径组；依据组合自动机的同步语义,从不可行路径组里抽取不可行组合路径片段,从而在后续路径遍历过程中规避包含这些片段的路径。实验显示该方法提高了组合系统可达性检验的效率。·提出了一种基于有界可达性检验结果推导出系统全局性质的途径。在有界可达性检验的过程中,会不断地收集到不可行子路径片段,当相关不可行子路径片段积累较多的时候,可能导致程序离散图结构上已经不存在能连通起点至目标点的潜在路径,在此情况下有界不可达性质可以进一步被推广到全局状态空间,并可以通过基于线性时序逻辑(Linear Temporal Logic, LTL)模型检验的方法来完成对该类问题的自动证明。·针对非线性混成自动机,提出了基于路径的有界可达性检验方法及相关优化技术。通过将路径可达性问题转换成一组带量词的非线性约束的可满足性问题,可以调用非线性约束求解器进行判定,在此基础上使用深度优先搜索依次枚举并验证阂值内的候选路径,从而完成有界可达性检验。进一步,提出了一种从非线性约束里抽取IIS的分析算法,可以从不可行的路径里定位出不可行子路径片段以约减状态空间。受限于当前底层支撑工具和非线性约束求解器的能力,所提方法目前仅得到可行性验证,其有效性还有待进一步的验证。