论文部分内容阅读
针对构件组合的状态爆炸问题，改进了反例引导的抽象精化框架，提出了组合式的抽象精化方法，使构件组合的模型检验转化为各成分构件的局部抽象精化，降低了分析的复杂度，提出了在构件组合情况下基于等价关系和存在商的构件抽象方法，用构件抽象的组合建立构件组合的抽象；提出了组合确认定理并给出证明，使反例确认分解为在各构件上对反例投影的确认；通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化，在模型检验构件组合的过程中，不需要为构件组合建立全局的具体状态空间。