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