2002/11/01 by Harry Li, Shriram Krishnamurthi, Kathi Fisler · 1 citation
Computer Science · #Advanced Software Engineering Methodologies #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Computer science #Feature (linguistics) #Software product line #Suite #Feature model #Software engineering #Model checking #Software #Runtime verification #Perspective (graphical) #Software system #Programming language #Formal verification #Software development #Artificial intelligence
paper · doi:10.1145/605466.605481
openalex publication_date 2002/11/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/06/11
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.