archives

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


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Liu, Jing (Janet), Basu, Samik and Lutz, Robyn (2008) Generating Variation-point Obligations for Compositional Model Checking of Software Product Lines. Technical Report 08-04, Computer Science, Iowa State University.

Full text available as:Adobe PDF

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.

Keywords:Software product lines, compositional model checking, variation point, feature
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
ID code:00000574
Deposited by:Jing (Janet) Liu on 21 May 2008



Contact site administrator at: ssg@cs.iastate.edu