Generating Variation-point Obligations for Compositional Model Checking of Software Product Lines

Date
2008-01-01
Authors
Liu, Jing
Basu, Samik
Lutz, Robyn
Journal Title
Journal ISSN
Volume Title
Publisher
Source URI
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

Software product lines are widely used due to their advantageous reuse of shared features while still allowing optional and alternative features in the individual products. Especially for high-integrity product lines, we would like to use model checking to verify that key properties hold as each new product is built. However, this goal is currently hampered by the complexity of composing model-checking results for the features in a way that allows reuse for subsequent products. This paper presents an incremental and compositional model-checking technique that allows efficient reuse of model checking results associated with the features in a product line. It goes beyond related work in that it removes restrictions on how the features can be sequentially composed. This flexibility is important because it means that many more real-world systems can be model-checked. We have implemented the technique, and demonstrate and evaluate it on a medical device product line.

Description
Keywords
Software product lines, compositional model checking, variation point, feature
Citation
Collections