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 Nov Times are displayed in time zone: Central Time (US & Canada) change
11:00 - 12:20: GPCE / SLE at SPLASH-III +12h Chair(s): Benoit CombemaleUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Eric Van WykUniversity of Minnesota, USA | |||
11:00 - 11:20 Talk | Automated Variability Injection for Graphical Modelling Languages GPCE Antonio GarmendiaJKU Linz, Manuel WimmerJKU Linz, Esther GuerraAutonomous University of Madrid, Elena Gómez-MartínezAutonomous University of Madrid, Juan de LaraAutonomous University of Madrid Link to publication DOI Pre-print Media Attached | ||
11:20 - 11:40 Talk | Modular and Distributed IDE SLE Fabien CoulonObeo, France / University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Alex AuvolatUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoit CombemaleUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Yérom-David BrombergUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, François TaïaniUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Olivier BaraisUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Noël PlouzeauUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France Link to publication DOI Pre-print Media Attached | ||
11:40 - 12:00 Talk | Correctness-by-Construction for Feature-Oriented Software Product Lines GPCE Link to publication DOI Media Attached | ||
12:00 - 12:20 Talk | A Family of Languages for Trustworthy Agent-Based Simulation SLE Link to publication DOI Pre-print Media Attached |
23:00 - 23:20 Talk | Automated Variability Injection for Graphical Modelling Languages GPCE Antonio GarmendiaJKU Linz, Manuel WimmerJKU Linz, Esther GuerraAutonomous University of Madrid, Elena Gómez-MartínezAutonomous University of Madrid, Juan de LaraAutonomous University of Madrid Link to publication DOI Pre-print Media Attached | ||
23:20 - 23:40 Talk | Modular and Distributed IDE SLE Fabien CoulonObeo, France / University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Alex AuvolatUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Benoit CombemaleUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Yérom-David BrombergUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, François TaïaniUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Olivier BaraisUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France, Noël PlouzeauUniversity of Rennes, France / Inria, France / CNRS, France / IRISA, France Link to publication DOI Pre-print Media Attached | ||
23:40 - 00:00 Talk | Correctness-by-Construction for Feature-Oriented Software Product Lines GPCE Link to publication DOI Media Attached | ||
00:00 - 00:20 Talk | A Family of Languages for Trustworthy Agent-Based Simulation SLE Link to publication DOI Pre-print Media Attached |