随着计算机系统规模和复杂度的不断增加，应用范围的不断扩大，人们对系统正确性的要求也日益提高。模型检验是一种形式验证技术，它的主要思想是构造系统的有限状态模型并穷尽搜索系统的整个状态空间以检验系统模型是否满足特定的性质。由于模型检验能够自动进行，并且在系统不满足性质时给出反例以帮助用户定位错误，它正在受到学术界和工业界越来越多的关注。由于符号化算法、偏序约简和抽象等技术的逐步发展成熟，模型检验技术已经可以处理相当规模的系统状态空间， Spin是一种被广泛应用的成熟的模型检验工具。它采用Promela语言作为系统建模语言和性质描述语言，具有强大的描述检验需求的能力，并且Spin中实现了现有先进的检验技术以确保检验过程的高效率。本文以Spin为基础，研究了检验以时段时序逻辑给出的系统规约和对并发C＃程序建模的问题，主要的工作包含以下方面： (1)针对目前在使用时段时序逻辑给出系统规约并进行检验的过程中存在的问题，提出了应当根据性质的直观含义确定其满足关系。我们将时段时序逻辑描述的性质分为两类，分别定义了它们各自的满足关系。进而，我们将这两种满足关系统一为一个更一般性的满足性定义，并以此为根据设计了相应的模型检验算法。使用该算法，我们可以利用已有的模型检验工具来检验以时段时序逻辑形式给出的系统规约。 (2)将上面的模型检验算法实现为基于时段时序逻辑的模型检验工具QRD-Checker。QRDChecker从以时段时序逻辑形式给出的系统规约构造相应的Promela时序声明，用于Spin检验。 (3)研究了从并发C＃程序构造检验模型的策略，提出了针对C＃程序中对象模型、语言模型和线程模型的翻译模型。C＃中的类通过Promela中的用户定义类型建模，静态变量通过全局变量建模；C＃中的方法、属性和索引器被内联到Promela程序中；C＃中的线程被对应到Promela中的进程，线程间的同步通过同步/异步信道上的消息通信建模。 (4)基于上面的翻译模型实现了并发C＃程序的模型抽取工具CSharp2Spin。CSharp2Spin能够自动根据并发C＃程序生成相应的Promela模型，Promela模型可以直接用于Spin检验。CSharp2Spin能够处理大部分C＃语言中的语法现象，具有一定的实用性。