Verifying cross-cutting features as open systems
Verifying cross-cutting features as open systems
复制标题
将横切功能验证为开放系统
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Kathi Fisler
中科院分区：
文献类型：
--
作者：
Harry C. Li;S. Krishnamurthi;Kathi Fisler
面向功能的软件设计捕获了许多有趣的交叉切割概念，并为建筑产品线体系结构提供了强大的方法。每个横切功能都是一个独立的模块，从验证的角度来看从根本上产生开放系统。我们描述了Desiderata，用于通过模型检查验证此类模块，并发现有关开放系统验证的现有工作未能解决以功能为导向的系统引起的大多数问题。因此，我们提供了一种验证此类系统的新方法。为了验证这种新方法，我们已经实施了它，并将其应用于表现出特征相互作用问题的一组模块。我们的模型检查器能够自动找到通过基于模拟的努力发现的十个先前发现的问题。
Feature-oriented software designs capture many interesting notions of cross-cutting, and offer a powerful method for building product-line architectures. Each cross-cutting feature is an independent module that fundamentally yields an open system from a verification perspective. We describe desiderata for verifying such modules through model checking and find that existing work on the verification of open systems fails to address most of the concerns that arise from feature-oriented systems. We therefore provide a new methodology for verifying such systems. To validate this new methodology, we have implemented it and applied it to a suite of modules that exhibit feature interaction problems. Our model checker was able to automatically locate ten problems previously found through a laborious simulation-based effort.