Modular Verification of Open Features Using Three-Valued Model Checking
Modular Verification of Open Features Using Three-Valued Model Checking
复制标题
使用三值模型检查对开放特征进行模块化验证
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Kathi Fisler
中科院分区：
文献类型：
--
作者：
Harry C. Li;S. Krishnamurthi;Kathi Fisler
面向对象的编程围绕特性而不是对象来组织程序，因此更好地支持可扩展的产品线架构。编程语言越来越多地支持这种编程风格，但程序员很少得到验证工具的支持。理想情况下，程序员应该能够相互独立地验证功能，并使用自动组合推理技术从其功能的属性中推断系统的属性。实现这一点需要精心设计的接口：它们必须包含足够的信息以支持组合验证，但工具应该能够自动生成这些信息，因为经验表明程序员不能或不会手动提供这些信息。我们提出了一个模型的接口，支持自动化，组合，面向特征的模型检查。为了证明它们的实用性，我们自动检测最初由Robert Hall在电子邮件套件案例研究中手动发现的功能交互问题。
Feature-oriented programming organizes programs around features rather than objects, thus better supporting extensible, product-line architectures. Programming languages increasingly support this style of programming, but programmers get little support from verification tools. Ideally, programmers should be able to verify features independently of each other and use automated compositional reasoning techniques to infer properties of a system from properties of its features. Achieving this requires carefully designed interfaces: they must hold sufficient information to enable compositional verification, yet tools should be able to generate this information automatically because experience indicates programmers cannot or will not provide it manually. We present a model of interfaces that supports automated, compositional, feature-oriented model checking. To demonstrate their utility, we automatically detect the feature-interaction problems originally found manually by Robert Hall in an email suite case study.