中文摘要：

模型检验是一种自动化验证技术，其应用主要的困难在于状态空间爆炸问题。针对构件组合形成的状态空间爆炸问题，结合构件抽象组合原理及反例引导的抽象精化框架，提出了一种测试用例自动生成的方法。根据某个待集成构件抽象已集成的其他构件，并通过组合各个抽象构件生成抽象组合模型。利用模型检验工具对组合模型进行集成测试，生成抽象测试用例，再通过精化得到原模型对应的具体测试用例。实验结果表明该方法减小了状态空间，在一定程度上减缓了状态空间爆炸的问题。

英文摘要：

Model checking is an approach to formal automation verification, whose difficulties are due to the state explosion problem. On an account of the space state explosion in components composition, propose a test case generation method, which combines the composi- tional reasoning theory and the counterexample guided abstraction refinement framework. According to a integrated component abstract the other integrated components, then generate abstract composition model by combining all abstract components. Generate abstract test cases by tools, finally correct test cases are generated by refining abstract models repeatedly. The experimental results indicate that the proposed approach can alleviate the state space explosion to some extent.