Trustworthy Variant Derivation with Translation Validation for Safety Critical Product Lines

Software product line (SPL) engineering facilitates development of entire families of software products with systematic reuse. Model driven SPLs use models in the design and development process. In the safety critical domain, validation of models and testing of code increases the quality of the products altogether. However, to maintain this trustworthiness it is necessary to know that the SPL tools, which manipulate models and code to derive concrete product variants, do not introduce errors in the process.

We propose a general technique of checking correctness of product derivation tools through translation validation. We demonstrate it using Featherweight VML—a core language for separate variability modeling relying on a single kind of variation point to define transformations of artifacts seen as object models. We use Featherweight VML with its semantics as a correctness specification for validating outputs of a variant derivation tool. We embed this specification in the theorem proving system Coq and develop an automatic generator of correctness proofs for translation results within Coq. We show that the correctness checking procedure is decidable, which allows the trustworthy proof checker of Coq to automatically verify runs of a variant derivation tool for correctness.

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.