Using Variability Models to Reduce Verification Effort of Train Station Models

We show how the effort needed to verify a transformed base model can be reduced by analyzing the definition of the modification. The Common Variability Language (CVL) is a generic language for modeling variability, where a CVL model describes the increment from one base model to another (transformed) base model. Assuming that a property of the base model has been verified, we use the CVL model to reduce the effort needed to verify the property of the transformed model. Based on the CVL model, we narrow down the set of traces required to be verified, including the increment and the cascading effects. We apply CVL to several models of the Train Control Language (TCL) to illustrate how the effort of verifying safety properties of transformed train station models can be reduced.