Trustworthy variant derivation with translation validation for safety critical product lines

We demonstrate how such a simple validation system can be constructed, by using this to validate variant derivation of a simple variability model implementation based on the Eclipse Modeling Framework. We hope that this presentation will encourage other researchers to use translation validation to validate more complex correctness properties in handling variability, as well as demonstrate to commercial tool vendors that formal verification can be introduced into their tools in a very lightweight manner.