模型检验是一种重要的自动化验证技术，在保障软件高可信性过程中发挥着巨大作用。近年来分布式系统的发展表明，模型检验中的公平性问题已经引起了诸多关注。如果不考虑公平性，模型检验常常会产生一些不现实的回路，比如某些进程或事件被调度器无限次地忽略，或者某些处理器永远比另外的处理器更快，而据此产生的反例并不是用户真正要找的系统缺陷。此外，随着模型检验的研究重点转向实时系统，学术界开始关注一类特殊的公平性问题，即实时系统中的空性检测，该问题会对系统的安全性验证和活性验证等结果产生消极影响，从而降低模型检验的正确性。本文围绕模型检验中的公平性问题展开讨论，重点研究了支持公平性验证的模型检验算法，实时系统中的空性检测算法，以及相关验证工具的开发等子问题。论文的主要工作及贡献如下:　　1.总结了学术界存在的多种公平性定义，并将其和模型检验技术相结合，把支持公平性的模型检验问题转化为在Bichi自动机中，查找一个可接受(acceptable)的并且同时满足公平性约束的无穷运行。在此基础上，扩展Tarjan的SCC算法来解决回路查找问题，并提出了一个支持公平性验证的模型检验算法和框架。该算法能根据不同的公平性条件，产生相应的输出。实验表明该算法非常有效且性能良好。　　2.模型检验方法的成功在很大程度上得益于验证工具的支持，而现有的模型检验工具对公平性问题的支持很不充分。因此，本文在模型验证工具PAT框架中开发了专门的公平性验证的模块，支持多类公平性约束，包括进程层面的强/弱公平，事件层面的强/弱公平以及全局强公平性等。该工具能以on-the-fly的方式对线性时序逻辑性质进行验证。通过对两组实验（人口协议模型和基准模型）的比较发现，PAT工具中的公平性算法在和SPIN的对比中占据很大的优势。　　3.时间自动机是一种对实时系统进行形式化建模和验证的重要技术，本文为解决时间自动机中的空性检测问题，定义了一类特殊的时间自动机CUB-TA，提出了基于CUB-TA的空性检测算法，该算法不需要在时钟带图中增加新的状态或时钟，所以能极大提高空性检测的效率。同时，还提出了一种将任意时间自动机转化成CUB-TA的算法，并从理论上证明了其正确性。实验结果表明，CUB-TA在基准模型中较为普遍，因此该方法非常具有实用性。　　4.如何把主流空性检测算法放到一个实用和公平的环境中进行对比分析，学术界目前还缺乏相关工作。本文开发了一个集成多种算法的模型检验工具TA@PAT，该工具中设计的启发式规则能根据不同的输入模型，自动选择最优算法进行计算。据我们所知，TA@PAT是目前唯一能直接支持基于空性检测的LTL性质验证的工具。此外，通过对多个基准模型进行实验，我们完成了一次系统而全面的空性检测算法的评估，并给出了相关的结论和分析。　　5.多层次的实时系统不能直接用时间自动机建模，为此学术界提出了一种新的建模语言——STCSP(Stateful Timed CSP)。为解决STCSP模型中的空性检测问题，本文提出了一种时钟对称化简方法，减小了时钟带图的大小，从而极大地改进了以往的空性检测算法的效率。此外，还将该算法集成进了模型验证工具PAT，以使其能支持面向STCSP模型的基于空性检测的LTL性质验证。