Revived web site previously available under

Fourth Workshop on Formal Methods and Analysis in Software Product Line Engineering
(FMSPLE 2013)

August 27, 2013.

Co-located with the 17th International Software Product Line Conference (SPLC 2013)
August 26-30, Tokyo, Japan


9:00-10:30 Invited Speaker
Systematic Derivation of Static Analyses for Software Product Lines
Andrzej Wąsowski
11:00-12:30 First Session
Variability-Aware Safety Analysis using Delta Component Fault Diagrams
Christoph Seidl, Ina Schaefer, Uwe Assmann
Combining Declarative and Procedural Views in the Specification and Analysis of Product Families
Maurice H. ter Beek, Alberto Lluch Lafuente, Marinella Petrocchi
A Methodology for Software Product Platform Design Based on Features
Hamad Alsawalqah, Sungwon Kang, Danhyung Lee
14:00-15:30 Second Session
Behavioral Refinement of Non-deterministic State Transition Diagrams based on Behavior Elimination
Christian Prehofer, Peter Scholz
Discrete Time Markov Chain Families: Modeling and Verification of Probabilistic Software Product Lines
Mahsa Varshosaz, Ramtin Khosravi
A Decision Table Analyzer for Detecting Variability in Source Code
Masahiro Sakai, Takeo Imai, Mikito Iwamasa, Takeshi Nagaoka and Mari Inoki
16:00-17:30 Panel Discussion
Future role of formal methods in software product line engineering:
Challenges, Open Problems, Perspectives
Participants TBD


Software product line engineering (SPLE) aims at developing a family of systems by reuse in order to reduce time to market and to 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 and analysis approaches 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 and analysis approaches 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 and Analysis 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 and analysis. So far, both communities are only loosely connected, despite very promising 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 and analysis approaches are currently applied in SPLE. This leads to a 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. 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 proposed workshop focuses on the application of formal methods and analysis approaches in all phases of SPLE, including domain and application engineering, in order to ensure the correctness of individual artifacts as well as the consistency among them. The topics of interest include, but are not limited to:


The FMSPLE workshop will be a full-day event, starting with a keynote presentation. 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 discussion of its participants 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 ACM two-column conference proceedings format (Letter) and be 4-8 pages of length.

The papers should be submitted via the EasyChair conference management system and will be 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.

Submission via Easychair.


Paper Submission: May 17, 2013May 31, 2013
Notification: June 10, 2013June 17, 2013
Camera-ready versions: June 28, 2013July 4, 2013
Workshop: August 27, 2013


Dave Clarke KU Leuven, Belgium (Chair)
Natsuko NodaNEC, Japan
Alice MillerUniversity of Glasgow, Scotland
Kathi FislerWorcester Polytechnic Institute, USA
Reiner HähnleTU Darmstadt, Germany
Martin LeuckerUniversity of Lübeck
Kim G. LarsenAalborg University, Denmark
Andreas ClassenIntec Software Engineering, Belgium
Patrick HeymansUniversity of Namur, Belgium
Maurice H. ter BeekISTI-CNR, Pisa, Italy
Ina SchaeferTechnische Universität Braunschweig, Germany
Stefania GnesiISTI-CNR, Pisa, Italy
Richard BubelTU Darmstadt, Germany
Ferruccio DamianiUniversità di Torino, Italy
Dirk BeyerUniversity of Passau, Germany
Dilian GurovKTH, Sweden
Atsushi IgarashiKyoto University, Japan


Ina Schaefer Technical University of Braunschweig, Germany
Maurice ter Beek ISTI-CNR, Pisa, Italy
Sven Apel University of Passau, Germany
Joanne Atlee University of Waterloo, Canada