A Tool-supported Technique for Specification & Management of Model-checking Properties for Software Product Lines

Liu, Jing (Janet), Hauptman, Miriam, Lutz, Robyn, Geppert, Birgit and Rößler, Frank (2007) A Tool-supported Technique for Specification & Management of Model-checking Properties for Software Product Lines. Technical Report 08-05, Computer Science, Iowa State University.

Abstract

Property specification in model checking is currently handled without adequately taking software product lines into account. This is largely due to the fact that the available model checkers and property specification tools lack sufficient support for reusing model-checking effort. The challenge is twofold: first, we need to make the properties accurately trace to individual system requirements and models even as they evolve; and second, we need to make the property specification easy to share and reuse among different systems of the same product line. The contribution of this work is a tool-supported technique to guide users in generating, selecting, managing, and reusing product-line properties and patterns of properties. The technique is evaluated in a product-line application. Results show that it improves the reusability and traceability of property specifications for model checking in a product line setting.