Editorial preface for the JLAMP Special Issue on Formal Methods for Software Product Line Engineering

This special issue is devoted to the themes of the FMSPLE workshop series on formal methods and analysis in Software Product Line Engineering (SPLE). SPLE aims at developing a family of (software) systems by reuse in order to reduce time-to-market and to increase product quality. The correctness of the artefacts intended for reuse, as well as the correctness of the developed products, is of crucial interest for many safety-critical or business-critical applications. Formal methods and analysis techniques have been successfully applied in single system engineering in order to rigorously establish critical system requirements. While SPLE has matured considerably over the last decade, many challenges still remain, among which efficient variability management, the consistency between domain and application engineering, the reduction of quality assurance efforts, and the consistent and sustainable evolution of product families. However, formal methods and analysis techniques are still not applied broadly enough in SPLE, despite their potential to improve product quality. One of the reasons for this is that existing formal approaches from single system engineering do not consider variability, the quintessential feature of product lines.