%0 Journal Article
%T 构件组合的抽象精化验证
%A 曾红卫？
%A 缪淮扣？
%J 软件学报
%P 1149-1159
%D 2008
%X 针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.
%K 构件组合
%K 模型检验
%K 状态爆炸
%K 等价关系
%K 反例引导的抽象精化
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20080507&flag=1