ITU

Trustworthy Variant Derivation with Translation Validation for Safety Critical Product Lines

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Standard

Trustworthy Variant Derivation with Translation Validation for Safety Critical Product Lines. / Iosif-Lazăr, Alexandru Florin; Wasowski, Andrzej.

In: The Journal of Logic and Algebraic Programming, Vol. 85, No. 6, 85, 24.11.2016, p. 1154–1176.

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{527091fc8b1e41c4bf3c73a85ebfdc3b,
title = "Trustworthy Variant Derivation with Translation Validation for Safety Critical Product Lines",
abstract = "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.",
author = "Iosif-Laz{\u a}r, {Alexandru Florin} and Andrzej Wasowski",
year = "2016",
month = nov,
day = "24",
doi = "10.1016/j.jlamp.2016.02.001",
language = "English",
volume = "85",
pages = "1154–1176",
journal = "Journal of Logic and Algebraic Programming",
issn = "2352-2208",
publisher = "Pergamon Press",
number = "6",

}

RIS

TY - JOUR

T1 - Trustworthy Variant Derivation with Translation Validation for Safety Critical Product Lines

AU - Iosif-Lazăr, Alexandru Florin

AU - Wasowski, Andrzej

PY - 2016/11/24

Y1 - 2016/11/24

N2 - 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.

AB - 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.

U2 - 10.1016/j.jlamp.2016.02.001

DO - 10.1016/j.jlamp.2016.02.001

M3 - Journal article

VL - 85

SP - 1154

EP - 1176

JO - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

SN - 2352-2208

IS - 6

M1 - 85

ER -

ID: 79303720