Events and Fairs

1st International Workshop on Formal Methods in Software Product Line Engineering

Co-located with the 14th International Software Product Line Conference (SPLC 2010)


Software product line engineering (SPLE) aims at developing a family of systems through reuse in order to reduce time to market and increase product quality. The correctness of the development artifacts 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, such as static analysis, model checking, or theorem proving, have been successfully applied in single system engineering over the last years in order to rigorously establish critical system requirements. However, in SPLE, formal methods are not broadly applied yet, despite their potential to improve product quality. One of the reasons is that existing formal approaches from single system engineering do not consider variability, an essential aspect of product lines.

The objective of the workshop “Formal Methods in Software Product Line Engineering (FMSPLE)” is to bring together researchers and practitioners from the SPLE community with researchers and practitioners working in the area of formal methods. So far, both communities have only been loosely connected, despite some initial work on formal analysis techniques for software product lines. The workshop aims at reviewing the state of the art and the state of the practice in which formal methods are currently applied in SPLE. Based on this, further application areas of formal methods in SPLE are identified, and practical requirements for the applicability of formal methods are established. This leads to the discussion of a research agenda for the extension of existing formal approaches and the development of new formal techniques for dealing with the particular needs of SPLE. Based on the workshop results, researchers will take up topics of interest to improve and extend the applicability of formal methods in SPLE, while practitioners will start using existing formal techniques in their organizational context to improve the quality of the developed products.
To achieve the above objectives, the workshop is intended as a highly interactive event fostering discussion and initiating collaborations between the participants from both communities. The workshop will serve as the starting point for a series of workshops on formal methods in SPLE to have the product line and formal methods communities join forces in order to advance the applicability of formal methods in SPLE.


The workshop focuses on the application of formal methods in all phases of SPLE, including family and application engineering, and on formal methods for ensuring the correctness and consistency of the artifacts considered in all phases of SPLE. The topics of interest include, but are not limited to:

  • Formal methods for variability modeling and analysis of feature models
  • Formal methods in domain analysis and scoping
  • Formal methods for product line architectures
  • Formal methods for component-based product line development
  • Formal methods for product line implementation, such as programming languages, formal language semantics, type systems
  • Formal verification of product lines and product line artifacts, including theorem proving, model checking, and static analysis techniques
  • Correctness-by-construction techniques applied in SPLE
  • Formal methods for non-functional properties in SPLE
  • Automated test case generation and formal testing in SPLE
  • Formal methods for product derivation and application engineering
  • Formal methods in model-based development of product lines
  • Tools and applications of formal methods in SPLE
  • Empirical evaluation and industrial experiences of applying formal methods in SPLE
  • Integration of formal methods into the software product line life-cycle
  • Formal methods for product line evolution

Workshop Program

0900h - 0915h Welcome by Organizers
0915h - 1030h Keynote by Mike Hinchey (Lero, Ireland): "Formally Developing Families of Space Exploration Missions"
1030h - 1100h Coffee Break
1100h - 1230h Session 1: Feature Modeling
Martínez and Gerardo Schneider.  Analysing Variability of Software Product Lines
Pim van den Broek, Ismênia Galvão and Joost Noppen. Merging Feature
Dave Clarke and Jose Proenca. Towards a Theory of Views for Feature Models
1230h - 1400h Lunch Break
1400h - 1530h Session 2: Modeling and Analysing Variability
Radu Muschevici, Dave Clarke and Jose Proenca. Feature Petri Nets
Pim van den Broek. Optimization of Product Instantiation using Integer Programming
Hamideh Sabouri and Ramtin Khosravi. An Effective Approach for Verifying Product Lines in Presence of Variability Models
1530h - 1600h Coffee Break
1600h - 1700h Session 3: Product Line Engineering
Dave Clarke, Nikolay Diakov, Reiner Hähnle, Einar Broch Johnsen, German Puebla, Balthasar Weitzel and Peter Wong. HATS - A Formal Software Product Line Engineering Methodology
Martin Becker, Soeren Kemmann and K.C. Shashidhar. Integrating Software Safety and Product Line Engineering using Formal Methods: Challenges and Opportunities
1700h - 1730h Closing Discussion "Practical and Theoretical Challenges of Formal Methods in SPLE"

Workshop Format and Submissions

The workshop is planned as a full-day event, starting with a keynote presentation (to be confirmed), by an expert in the area of formal methods applied in SPLE. The keynote will be followed by presentations of selected peer-reviewed papers. To foster interaction within the workshop, a discussant will be assigned to each presented paper. The task of the discussant will be to prepare a summary of the paper and initiate the discussion of its results. The workshop will close with a panel discussion moderated by the organizers to summarize the state of the art and the state of the practice as presented in the workshop, to collect research challenges for the application of formal methods in SPLE, and to identify research topics for future workshops.

The contributed papers are expected to comprise research papers containing novel and previously unpublished results, experience reports, reports of industrial case studies, tool descriptions, and short papers describing work in progress or exploratory ideas. All papers have to follow the IEEE two-column conference proceedings format and be 4 - 8 pages of length. The papers will be submitted via the EasyChair conference management system and reviewed by at least three members of the program committee. The program committee will select the best papers based on quality, relevance to the workshop, and potential to initiate discussions for presentation. The workshop proceedings will be published in the second volume of the SPLC proceedings. 

Important Dates

  • Workshop Paper Submission: June 15
  • Workshop Paper Notification: July 9
  • Camera-ready Copy of Papers: July 19
  • Workshop: September 14

Program Committee

Ina Schaefer (Chalmers, SE) (Co-Chair)
Gerardo Schneider (U Gothenburg, SE)
Martin Becker (IESE, DE)
Ralf Carbon (IESE, DE) (Co-Chair)
Sven Apel (U Passau, DE)
Dirk Muthig (Lufthansa Systems, DE)
Frank van der Linden (Philips, NL)
Frank de Boer (CWI, NL)
Dave Clarke (KU Leuven, BE)
Patrick Heymans (Namur, BE)
Manfred Broy (U Munich, DE)
Tomoji Kishi (Waseda University, JP)
John McGregor (Clemson University, US)
Mark Staples (NICTA, AU)
David Benavides (U Seville, ES)
Natsuko Noda (NEC, JP)


Main Organizer:

Ina Schaefer
Chalmers University of Technology
Department of Computer Science and Engineering
412 96 Gothenburg, Sweden
Phone: + 46 - 31 - 772 - 1072


  • Martin Becker
    Fraunhofer IESE, Kaiserslautern, Germany
  • Ralf Carbon
    Fraunhofer IESE, Kaiserslautern, Germany
  • Sven Apel
    Universität Passau, Passau, Germany