信息技术的飞速发展，使软件产品应用到社会的各个领域，软件产品的质量自然成为人们共同关注的焦点。软件测试在整个软件开发的过程中占有重要的地位。传统的手工测试代价昂贵，迫切需要测试过程的自动化。基于模型的测试使得测试自动化成为可能，这也将大大降低软件测试的成本。基于模型的测试是一种有效的软件测试方法，它使用行为模型描述待测系统(system under test, SUT)的期望行为和环境的可能行为。模型的输入输出对作为实际系统的测试用例，其中，模型的输出是待测系统的期望输出。在基于模型的测试中应用模型检验技术自动生成测试用例是一个研究热点。本文的工作主要包括四个方面：第一，基于模型的测试生成的测试用例集通常会产生大量冗余的测试用例，这样会大大增加测试执行的代价。针对测试用例集生成过程中测试用例约简的问题进行了研究，提出了一种基于可满足性理论的测试用例集约简方法。采用EFSM描述系统模型，用LTL描述测试目标，按测试目标对应的CNF公式的难度选择生成测试用例的测试目标，采用模型检验技术生成测试用例，根据可满足性理论判定生成的测试用例是否覆盖了未生成测试用例的测试目标，以达到测试用例的约简。第二，我们研究了采用反例制导的抽象精化的方法如何在第一部分工作的基础上进一步约简测试用例集。提出了采用公式簇定义EFSM模型中状态的等价类，生成原始EFSM的抽象模型。在抽象模型上采用模型检验技术生成抽象反例。如果生成的抽象反例为伪反例，根据反例制导的抽象精化技术精化模型。最后在最终的抽象模型上使用本文提出的基于可满足性的方法生成约简的测试用例集。第三，采用模型检验技术生成的测试用例只是状态序列，而完整的测试用例还应该包含测试数据和期望输出。为了使得生成的测试用例能够真正地执行，必须对其实例化。本文提出了一种为EFSM模型中的路径生成测试数据的方法。Kalaji的方法采用遗传算法生成测试数据，我们分析了Kalaji的方法的不足，对它进行了改进，在计算个体适应度时同时考虑了它的分支距离和未覆盖条件的比率。第四，使用随机方法生成的测试路径(状态序列)有很多是不可行的，而为这些不可行的路径去生成测试数据是一件浪费时间的事情。我们考虑了EFSM中路径的可行性问题。采用切片技术获取与指定迁移相关的迁移集，给出了应用定理证明技术判定路径是否可行的方法。此外，本文还对所提出的方法进行了详细的实验评价，验证了方法的有效性。最后，使用一个基于组件的系统——自控镇痛泵系统来系统地说明论文中提出的方法。对该系统进行了简单的描述并给出了系统中主要组件的EFSM模型。采用反例制导的抽象精化方法生成各个组件的抽象模型，对各个组件的抽象模型进行并行组合，得到抽象的并行组件模型，使用基于可满足性的方法生成抽象的并行组合模型的约简测试用例集，根据我们提出的方法为每条测试用例生成测试数据。