Managing evolution in Software Product Lines: A model-checking perspective

In Software Product Line (SPL) engineering, similar software products are developed in families rather than individually. Developing similar software at once leads to new challenges. In particular, the model checking problem for SPL is harder because it has to deal with potentially many products and identify exactly which ones do not work properly. In previous work, we introduced Featured Transition Systems as a compact behavioural model for SPL. We also proposed new algorithms that model check all the products of the SPL efficiently, by taking into account the commonality between them to reduce the verification time. However, our current approach does not consider that SPL can evolve. If a new feature is added to the SPL, previous verification results cannot be reused. In this paper, we define formally two particular classes of features. Using simulation relations, we show that we may anticipate the properties of some products introduced by those features. We discuss interesting perspectives and present the challenges that are still ahead. Copyright 2012 ACM.