摘要
针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.
This paper addresses the state-space explosion problem in the context of verifying component composition. It adapts the counterexample guided abstraction refinement （CEGAR） scheme and proposes a compositional verification approach that the verification of component composition is transformed into local abstraction refinement for individual components participating in the composition in order to reduce analysis complexity. The existential quotient based on equivalence relation is employed to compute the abstraction of each component in component composition, and then the abstraction model for the component composition can be built by composing the existential quotients of components. A compositional validation theorem is proposed and proved, so validating if a generated counterexample is valid and refining the abstraction are all carried out component-wise. This approach does not require the construction of a complete state space of the concrete component composition under verification.
出处
《软件学报》
EI
CSCD
北大核心
2008年第5期1149-1159,共11页
Journal of Software
基金
国家自然科学基金No.60673115
国家高技术研究发展计划(863)No.2007AA01Z144
国家重点基础研究发展计划(973)Nos.2002CB310800
2002CB312001
上海市教委科研项目No.07ZZ06
上海市重点学科建设项目No.J50103~~
关键词
构件组合
模型检验
状态爆炸
等价关系
反例引导的抽象精化
component composition
model checking
state explosion
equivalence relation
counterexample guidedabstraction refinement
