Potential synergies of theorem proving and model checking for software product lines
Potential synergies of theorem proving and model checking for software product lines
复制标题
软件产品线的定理证明和模型检查的潜在协同作用
DOI：
10.1145/2648511.2648530
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
A. von
中科院分区：
文献类型：
--
作者：
Meinicke;Benduhn;Hentschel;A. von
软件产品线的验证是一个活跃的研究领域。一个挑战是有效地验证类似的产品，而不需要单独生成和验证它们。作为解决方案，研究人员提出了基于族的验证方法，该方法将编译时的可变性转换为运行时的可变性，或者使验证工具具有可变性。现有的方法要么集中在定理证明，模型检查，或其他验证技术。我们首次将联合收割机定理证明和模型检测结合起来，评估它们在产品线验证中的协同作用。我们通过连接五个现有的工具来提供工具支持，即用于产品线开发的KubureIDE和KubureHouse，以及用于验证Java程序的KeY，JPF和OpenJML。在一个实验中，我们发现了提高效率和效率的协同作用，特别是对于缺陷很少的产品线。此外，我们发现，如果产品线包含更多的缺陷，模型检查和定理证明会更有效。
The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches, which either transform compile-time into runtime variability or make verification tools variability-aware. Existing approaches either focus on theorem proving, model checking, or other verification techniques. For the first time, we combine theorem proving and model checking to evaluate their synergies for product-line verification. We provide tool support by connecting five existing tools, namely FeatureIDE and FeatureHouse for product-line development, as well as KeY, JPF, and OpenJML for verification of Java programs. In an experiment, we found the synergy of improved effectiveness and efficiency, especially for product lines with few defects. Further, we experienced that model checking and theorem proving are more efficient and effective if the product line contains more defects.
登录
查看更多内容
管理克隆产品变体的框架
DOI：
10.1109/icse.2013.6606686
发表时间：
2013
期刊：
2013 35th International Conference on Software Engineering (ICSE)
影响因子：
--
作者：
J. Rubin;M. Chechik
通讯作者：
M. Chechik
事件 B 中面向特征的建模基础
DOI：
10.1007/978-3-642-11811-1_42
发表时间：
2010
期刊：
2012 19th Working Conference on Reverse Engineering
影响因子：
--
作者：
J. Sorge;M. Poppleton;M. Butler
通讯作者：
M. Butler
影响因子：
16.6
作者：
Thuem, Thomas;Apel, Sven;Saake, Gunter
通讯作者：
Saake, Gunter
技术转让软件工具手稿编号（将由编辑插入）使用可扩展软件模型检查框架检查 JML 规范⋆
DOI：
10.1007/s10009-005-0218-5
发表时间：
2006
影响因子：
1.5
作者：
N. Polikarpova;Julian Tschannen;Carlo A. Furia
通讯作者：
Carlo A. Furia
DOI：
10.1007/bfb0031813
发表时间：
1996-08
期刊：
--
影响因子：
--
作者：
N. Shankar
通讯作者：
N. Shankar