随着软件规模不断扩大,内部结构愈发复杂,应用环境日益开放,软件可信性已成为人们广泛关注的热点。在软件开发的不同阶段,软件可信性呈现出各种属性形态,涵盖正确性、可靠性、安全性等,它是软件诸多属性的综合体现。如何验证软件可信性是可信软件的关键研究领域,采用模型检测技术验证软件的时序正确性是其中一个极其重要的研究方向。软件模型检测是形式化证明软件是否满足期望性质的算法类验证方法,其自动化程度高,当软件违反期望性质时还会给出一个系统反例。由于系统模型随变量数或并发组件数等因素的线性增长呈指数级增长,且软件模型检测穷尽搜索系统模型的状态空间以寻找反例,因此模型检测可能无法在期望的时空开销内完成验证,即产生状态空间爆炸问题。控制状态空间爆炸始终是软件模型检测的一个重大研究方向。状态空间爆炸存在于面向系统模型的静态模型检测,也存在于基于程序执行的动态模型检测。在LTL(Linear Temporal Logic)静态模型检测领域,on-the-fly自动机理论的LTL模型检测是一种有效缓解状态爆炸的方法。它首先将LTL性质翻译成与其否定公式等价的ω-自动机,然后将LTL模型检测问题转化成ω-自动机的空性检测问题,即系统模型和否定性质自动机的同步积ω-自动机,并且采用on-the-fly方式空性检测,若积自动机非空,该方法无需建立整个积空间就能找到反例。通常LTL性质翻译涉及B(?)chi自动机和广义B(?)chi自动机两种ω-自动机,同时,空性检测方法分为顺序和并行两类计算模式,在这几类on-the-fly空性检测方法中仍有许多待研究的重要挑战。在并发软件的动态模型检测领域,并发线程的交织爆炸会导致执行状态空间爆炸,有状态动态偏序归约方法能有效缩减交织数量,但该方法的计算性能仍有待提高。本文立足软件模型检测方法,重点围绕on-the-fly自动机理论的LTL模型检测中三类空性检测方法,以及动态模型检测中有状态动态偏序归约方法,分别针对这四种模型检测方法存在的具体问题,开展如下研究,以进一步提升模型检测方法的性能:(1)针对NDFS(Nested Depth-First Search)B(?)chi自动机空性检测返回不必要的长反例问题,其妨碍反例理解且倾向于消耗较多时空代价,提出一种on-the-fly深度有界的B(?)chi自动机空性检测方法。它利用深度有界缩减策略约束NDFS方法,使其遍历有界积空间。首先深度有界缩减策略设定积自动机的状态最小深度为受限参数,并增量完备地计算有界积状态集,然后利用NDFS穷尽遍历on-the-fly生成的有界积空间以寻找反例。实验结果表明,该方法普遍适用于积自动机非空的情况,能有效返回较优短反例,产生的时空代价与同类算法相当。(2)针对全面结合位状态哈希的SCC(Strongly Connected Components)广义B(?)chi自动机空性检测方法对于SCC合并的终止条件考虑不全面的问题,提出位状态哈希终端SCC的on-the-fly广义B(?)chi自动机空性检测方法。首先形式化给出终端SCC的定义,然后针对完全遍历的终端SCC采用位状态哈希技术。理论证明了方法的正确性,而且实验结果表明该方法覆盖了 SCC合并终止的所有情况,缩减了空性检测的内存消耗。在此方法基础上,再融入复合启发式策略,提出位状态哈希终端SCC的on-the-fly启发式广义B(?)chi自动机空性检测方法。复合启发式将每个状态的所有后继迁移分成四个等级,每次优先选择最高等级的一个迁移执行积空间遍历。实验结果表明,该方法进一步提高了广义B(?)chi自动机空性检测的时空性能,相比同类算法,其性能更优。(3)针对一种结合最大接受前驱的on-the-fly并行空性检测方法,其面对传播的接受环最大接受前驱处于环外的情境,无法通过传播接受前驱识别接受环的问题。提出一种传播最大和最新接受前驱的on-the-fly并行空性检测方法。在首次遍历积自动机图时,它采用最大接受前驱和最新接受前驱的双值传播模式,最大接受前驱仍保留原方法的传播特征,引入的最新接受前驱追踪并行空性检测的局部遍历特征。大量实验结果表明,在显现on-the-fly优势的提前终止率方面,所提方法高于原始方法,因此在原始方法on-the-fly识别失效时该方法仍能成功识别接受环,且该方法提高了并行空性检测的时空性能。(4)无状态或有状态的动态偏序归约方法在验证多线程并发程序时,候选回溯集的计算是更新回溯集的关键步骤之一,实际上原始候选回溯集的计算成本超出了回溯集的更新需求。针对上述问题,提出收缩候选回溯集的有状态动态偏序归约方法。设收缩候选回溯条件二为回溯点后首个与待执行迁移存在发生先序关系的使能迁移,因此当前交织中至多一个迁移满足它,故收缩候选回溯集去掉了满足原始回溯条件二的冗余迁移。进而该方法利用收缩候选回溯集更新回溯集,有效实现了有状态动态偏序归约模型检测。实验结果表明,该方法降低了遍历迁移数,加速了回溯集更新,提高了动态模型检测效率。