首页> 外文期刊>Journal of Logic and Algebraic Programming >Incremental model checking of delta-oriented software product lines
【24h】

Incremental model checking of delta-oriented software product lines

机译:面向增量软件产品线的增量模型检查

获取原文
获取原文并翻译 | 示例

摘要

We propose DeltaCCS, a delta-oriented extension to Milner's process calculus CCS to formalize behavioral variability in software product line specifications in a modular way. In DeltaCCS, predefined change directives are applied to core process semantics by overriding the CCS term rewriting rule in a determined way. On this basis, behavioral properties expressed in the Modal μ-Calculus are verifiable for entire product-line specifications both product-by-product as well as in a family-based manner as usual. To overcome potential scalability limitations of those existing strategies, we propose a novel approach for incremental model checking of product lines. Therefore, variability-aware congruence notions and a respective normal form for DeltaCCS specifications allow for a rigorous local reasoning on the preservation of behavioral properties after varying CCS specifications. We present a prototypical DeltaCCS model checker implementation based on Maude and provide evaluation results obtained from various experiments concerning efficiency tradeoffs compared to existing approaches.
机译:我们提出DeltaCCS,这是Milner的过程演算CCS的面向增量的扩展,以模块化的方式形式化软件产品线规格中的行为可变性。在DeltaCCS中,通过以确定的方式覆盖CCS术语重写规则,将预定义的更改指令应用于核心流程语义。在此基础上,模态μ演算中表达的行为特性可针对整个产品线规格进行验证,包括逐个产品以及照常以家庭为基础。为了克服这些现有策略的潜在可伸缩性限制,我们提出了一种用于产品线增量模型检查的新颖方法。因此,DeltaCCS规范的可变性意识一致概念和相应的范式允许在更改CCS规范后对行为特性的保留进行严格的本地推理。我们提出了一个基于Maude的原型DeltaCCS模型检查器实现,并提供了与现有方法相比从各种效率折衷实验获得的评估结果。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号