在计算机科学迅猛发展的今天,云计算、物联网、移动互联网成了时代的标志,这些软件技术的高速发展对自身验证的可靠性和硬件性能提出了挑战,对于硬件的性能要求最终落到了硬件集成电路的可靠性上面。然而,在硬件发展的历程中,验证集成芯片的正确性和可靠性一直是一个瓶颈。在验证领域使用最多的是基于模拟的验证方式,这种检验方式存在其不可弥补的缺点,即它只能证明系统有错,而不能证明系统设计的正确性。而在软件方面,对于可靠性的验证还处于没有形成特定规范的阶段。所以无论是针对软件还是硬件,对其可靠性的验证都是有实质意义的。本文主要以半张量积为数学理论,研究一种基于半张量积的模型检测算法。算法主要分为三个部分:被验证系统的数学建模、被验证系统需要满足的属性描述和模型检测算法。针对被验证系统数学建模,首先根据被验证系统的原子集合,固定原子公式顺序,考查原子公式的取值,确定原子公式在系统状态的取值情况,定义系统状态的布尔编码表示。然后使用矩阵半张量积的逻辑抽象方法对系统状态向量化,得到系统的状态向量。根据规定系统状态的顺序,利用图论的邻接矩阵定义被验证系统的结构矩阵。最后使用向量乘法描述系统运行状态,并给出模型检测算法的正确性和有穷性的数学证明。本算法对被检测的属性的描述采用分支时态逻辑的计算树逻辑,因此分析了计算树逻辑(Computation Tree Logic,CTL)的适当集,选取相应的适当集对任意CTL公式进行标准化描述。针对CTL的适当集的原子语义EX、EG和EU分别给出了验证算法描述,再被验证系统需要满足的属性描述对任意CTL公式表示进行属性的复合语义验证算法设计方案。论文最后给出了基于半张量积的模型检测算法的应用实例分析,实现了从属性分析、模型建立到最后的验证,并完成了实例的验证工作。从应用实例表明,本算法不仅可以应用于软件系统和硬件系统的验证,还可以拓展到布尔网络分析等其他研究领域。