随着计算机软硬件系统规模的日益复杂化，如何保证计算机系统的正确性和可靠性，逐渐成为当前理论界和产业界共同关心的重要问题。而当前限制计算机实际广泛应用的因素已经不再是机器硬件“缓慢”的速度和“低下”的计算能力，而更多的是我们在设计和实现复杂系统时，设计与验证的能力还比较有限，无法保证所设计系统的正确性和可靠性。而基于状态搜索的模型检查技术为系统验证提供了有效的保证手段。 模型检查是一种针对有限状态并发系统的形式化验证技术，其基本思想是构造系统的有限状态模型，在系统模型的状态空间内运算，检查建立的系统模型是否满足期望的性质。本文考察模型检查技术的基本原理，研究模型检查在软件验证上的应用，并开发实现了一个针对C语言编写的程序进行验证的系统原型。并且按照存在量词公式的证据是全称量词公式的反例的特性，用模型检查的反例生成机制对测试用例生成技术进行研究，然后把模型检查的算法引入到软件测试领域，寻找满足规格说明的路径，生成测试用例，据此对系统进行测试。 本文的主要工作主要有： 1．研究模型检查技术，考察时序逻辑公式的特点，改进并实现模型检查的符号算法，开发一个针对CTL公式的模型检查器。 2．研究模型检查在C语言中的应用，提出把程序源代码作为模型检查的输入数据，直接对程序代码进行模型检查。 3．开发一个软件验证系统原型，实现从代码直接转换成状态迁移系统。 4．考察时序逻辑算子，根据存在量词公式和全称量词公式的转换关系，生成反例路径，生成测试用例，用于软件测试。