Correctness-by-Construction for Feature-Oriented Software Product Lines
Sun 15 Nov 2020 23:40 - 00:00 at SPLASH-III - Chair(s): Sheng Chen
Software product lines are increasingly used to handle the growing demand of custom-tailored software variants. They provide systematic reuse of software paired with variability mechanisms in the code to implement whole product families rather than single software products. A common domain of application for product lines are safety-critical systems, which require behavioral correctness to avoid dangerous situations in-field. While most approaches concentrate on post-hoc verification for product lines, we argue that a stepwise approach to create correct programs may be beneficial for developers to manage the growing variability. Correctness-by-construction is such a stepwise approach to create programs using a set of small, tractable refinement rules that guarantee the correctness of the program with regard to its specification. In this paper, we propose the first approach to develop correct-by-construction software product lines using feature-oriented programming. First, we extend correctness-by-construction by two refinement rules for variation points in the code. Second, we give a proof for the soundness of the proposed rules. Third, we implement our technique in a tool called VarCorC and show the applicability of the tool by conducting two case studies.
Sun 15 NovDisplayed time zone: Central Time (US & Canada) change
11:00 - 12:20 | SLE / GPCE at SPLASH-III +12h Chair(s): Benoit Combemale University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Eric Van Wyk University of Minnesota, USA | ||
11:00 20mTalk | Automated Variability Injection for Graphical Modelling Languages GPCE Antonio Garmendia JKU Linz, Manuel Wimmer JKU Linz, Esther Guerra Autonomous University of Madrid, Elena Gómez-Martínez Autonomous University of Madrid, Juan de Lara Autonomous University of Madrid Link to publication DOI Pre-print Media Attached | ||
11:20 20mTalk | Modular and Distributed IDE SLE Fabien Coulon Obeo, France / University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Alex Auvolat University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoit Combemale University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Yérom-David Bromberg University of Rennes, France / Inria, France / CNRS, France / IRISA, France, François Taïani University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Olivier Barais University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Noël Plouzeau University of Rennes, France / Inria, France / CNRS, France / IRISA, France Link to publication DOI Pre-print Media Attached | ||
11:40 20mTalk | Correctness-by-Construction for Feature-Oriented Software Product Lines GPCE Link to publication DOI Media Attached | ||
12:00 20mTalk | A Family of Languages for Trustworthy Agent-Based Simulation SLE Link to publication DOI Pre-print Media Attached |
23:00 - 00:20 | |||
23:00 20mTalk | Automated Variability Injection for Graphical Modelling Languages GPCE Antonio Garmendia JKU Linz, Manuel Wimmer JKU Linz, Esther Guerra Autonomous University of Madrid, Elena Gómez-Martínez Autonomous University of Madrid, Juan de Lara Autonomous University of Madrid Link to publication DOI Pre-print Media Attached | ||
23:20 20mTalk | Modular and Distributed IDE SLE Fabien Coulon Obeo, France / University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Alex Auvolat University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoit Combemale University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Yérom-David Bromberg University of Rennes, France / Inria, France / CNRS, France / IRISA, France, François Taïani University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Olivier Barais University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Noël Plouzeau University of Rennes, France / Inria, France / CNRS, France / IRISA, France Link to publication DOI Pre-print Media Attached | ||
23:40 20mTalk | Correctness-by-Construction for Feature-Oriented Software Product Lines GPCE Link to publication DOI Media Attached | ||
00:00 20mTalk | A Family of Languages for Trustworthy Agent-Based Simulation SLE Link to publication DOI Pre-print Media Attached |