构件组合的抽象精化验证

摘要：

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

关键词：构件组合、模型检验、状态爆炸、等价关系、反例引导的抽象精化

所属期刊栏目：19

分类号：TP311(计算技术、计算机技术)

资助基金：the National Natural Science Foundation of China under Grant No.60673115;the National High-Tech Research and Development Plan of China under Grant No.2007AA01Z144 国家高技术研究发展计划863;the National Basic Research Program of China under Grant Nos.2007CB310800, 2002CB312001 国家重点基础研究发展计划973;the Research Program of Shanghai Education Committee of China under Grant No.07ZZ06;the Shanghai Leading Academic Discipline Project of China under Grant No.J50103

在线出版日期：2008-07-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：1149-1159