混成系统是一类有广泛应用的基于计算机的系统，当前混成自动机是其主要设计建模语言，对混成自动机进行可达性检验是提高系统设计质量的重要途径。目前混成自动机的可达性检验途径主要包括通过空间几何计算技术计算完整系统可达状态集进行检验，以及通过SMT（Satisfiability Modulo Theories）技术对系统在给定阈值内行为进行编码并求解以实现有界可达性检验两种。但这两种途径均直接面向系统完整状态空间或者阈值内所有状态空间，在可检验系统的规模上受到很大的限制，离工业界的实际应用需求尚有相当大的距离。　　为了满足工业界的实际应用需求，增大可检验系统的规模，本文从一个新的角度对混成系统可达性检验问题展开研究:通过将有界可达性问题分解成各路径的可达性问题来降低问题规模并控制问题的复杂度，在此基础上结合路径遍历技术完成阈值内全状态空间的检验。本文主要工作包括以下几个方面:　　从面向路径可达性检验的角度对线性混成自动机以及线性混成自动机组合中单条路径或者单个路径集的可达性问题进行了研究。通过将路径可达性问题进行线性编码，将此问题转换成一组线性约束的可满足性问题从而调用成熟的线性规划技术进行求解。借助线性规划技术的强大性能，根据此方法我们可以开发有效的面向路径可达性检验工具，从而对大规模复杂路径进行验证并帮助设计人员在设计阶段对系统中关键路径进行分析，保障系统的质量。　　通过对系统图形结构进行快速遍历，对所遍历的每一条路径的可达性进行检验，实现了线性混成自动机的有界可达性检验技术。通过将大规模问题拆分成多个路径的可达性问题并依次分析，可以通过有限的资源来大规模系统进行判定，使得对复杂线性混成系统的检验成为可能。基于以上方法，开发了面向线性混成自动机的有界可达性检验工具BACH。通过实验显示，在检验大规模系统时，BACH表现了良好的处理能力与扩展能力。　　根据偏序缩减技术提出一种新的组合语义-浅同步语义，并在此基础上对线性混成自动机组合的有界模型检验问题给出了一种新的SMT编码方式。通过为每个成员自动机分别赋予各自独立的阈值与步长，对各个自动机分别编码然后再增加相应的同步约束，从而规避经典SMT编码中由交叠语义（强同步语义）所带来的大规模同步约束以及大量的中间约束，精简需要处理的约束集。实验结果显示，此编码方式的实验效果普遍优于现有交叠语义下的编码方式。　　将面向路径可达性检验算法从线性混成自动机领域向非线性领域进行了拓展。定义了一类非线性混成自动机-凸性混成自动机，并在其基础上提出了面向路径可达性验证方法。通过凸性约束编码将自动机上单条路径的面向路径可达性问题转换成一组凸性约束的可满足性问题。通过使用非线性数值分析领域高效的凸性规划技术，可以对该约束集的可满足性问题问题给出有效判定从而回答相应的面向路径可达性问题。实验显示，此方法可以检验的路径和系统无论是从路径长度上还是系统维度上都可以满足实际应用的需要。在此以外，进一步对本技术在更一般化的非线性混成自动机模型检验上的应用前景与方向进行了探索与研究。