Published: 28th March 2016
DOI: 10.4204/EPTCS.206
ISSN: 2075-2180


Proceedings 7th International Workshop on
Formal Methods and Analysis in Software Product Line Engineering
Eindhoven, The Netherlands, April 3, 2016

Edited by: Julia Rubin and Thomas Thüm

Julia Rubin and Thomas Thüm
Keynote Talk: Reasoning about Product Lines of Cyber-Physical Systems with Clafer
Krzysztof Czarnecki
Refactoring Delta-Oriented Product Lines to achieve Monotonicity
Ferruccio Damiani and Michael Lienhardt
Conflict Detection for Edits on Extended Feature Models using Symbolic Graph Transformation
Frederik Deckwerth, Géza Kulcsár, Malte Lochau, Gergely Varró and Andy Schürr
Incremental Consistency Checking in Delta-oriented UML-Models for Automation Systems
Matthias Kowal and Ina Schaefer
Analysis of Feature Models Using Alloy: A Survey
Anjali Sree-Kumar, Elena Planas and Robert Clarisó
Towards a Feature mu-Calculus Targeting SPL Verification
Maurice H. ter Beek, Erik P. de Vink and Tim A. C. Willemse


This volume contains the proceedings of FMSPLE 2016, the 7th International Workshop on Formal Methods and Analysis in Software Product Line Engineering, held in conjunction with ETAPS'16 on April 3, 2016 in Eindhoven, the Netherlands.

In Software Product Line Engineering (SPLE), a portfolio of similar systems is developed from a shared set of software assets. Claimed benefits of SPLE include reductions in the portfolio size, cost of software development and time to production, as well as improvements in the quality of the delivered systems. Yet, despite these benefits, SPLE is still in the early adoption stage. We believe that automated approaches, tools and techniques that provide better support for SPLE activities can further facilitate its adoption in practice and increase its benefits.

To promote work in this area, the FMSPLE 2016 workshop focused on automated analysis and formal methods, which can (1) lead to a further increase in development productivity and reduction in maintenance costs associated with management of the SPLE artifacts, and (2) provide proven guarantees for the correctness and quality of the delivered systems. More specifically, the workshop aimed at reviewing the state-of-the-art and the state-of-the-practice of analyses and formal methods for SPLE. It also aimed at soliciting examples for successful deployment of such techniques and discussing a research agenda for the next steps.

This year, the workshop included a keynote talk by Prof. Krzysztof Czarnecki, University of Waterloo, Canada: "Reasoning about Product Lines of Cyber-Physical Systems with Clafer". The abstract of the talk is provided as part of these proceedings.

We would like to express our gratitude to the keynote speaker and to the authors of all submitted papers for their contribution to the success of this workshop. We thank the members of the program committee for their work on the evaluation and discussion of the submitted papers. Finally, we would like to thank the workshop Steering Committee members, ETAPS organizers, and, specifically, the ETAPS workshop chair Erik de Vink, for their help throughout all stages of preparing and running the workshop.

Julia Rubin and Thomas Thüm
FMSPLE Co-Chairs

Program Committee

Steering Committee

Reasoning about Product Lines of Cyber-Physical Systems with Clafer

Krzysztof Czarnecki (University of Waterloo, Canada)

Abstract: Cyber-physical systems (CPS) combine complex machines, computers, networks, and people and are poised to change how we interact with the physical world. Example CPS include self-driving cars and intelligent buildings. Elements of CPS are often engineered as product lines in order to fit different contexts and markets. Computer modeling is essential to engineering such systems as analyzing and evolving virtual blueprints is easier and more cost-effective than performing these tasks on physical models or systems.

Clafer is a lightweight modeling language for modeling CPS architecture with dedicated support for variability modeling. I will illustrate a range of modeling and analysis tasks that can be performed using Clafer, including synthesis and multi-objective optimization of architectures and behavioral modeling and analysis in the presence of product-line variability. I will also discuss how domain-specific languages can be built on top of Clafer in order to improve usability for a given application domain. I will close with discussion of research challenges and suggestions for future work.

Short bio: Krzysztof Czarnecki is a Professor of Electrical and Computer Engineering at the University of Waterloo. Before coming to Waterloo, he was a researcher at DaimlerChrysler Research (1995-2002), Germany, focusing on improving software development practices and technologies in enterprise, automotive, and aerospace domains. He co-authored the book on "Generative Programming" (Addison-Wesley, 2000), which deals with automating software component assembly based on domain-specific languages. While at Waterloo, he held the NSERC/Bank of Nova Scotia Industrial Research Chair in Requirements Engineering of Service-oriented Software Systems (2008-2013) and has worked on a range of topics in model-driven systems and software engineering, including product line engineering, design exploration and synthesis, variability modeling, model transformation, and domain-specific languages. He has also helped automotive and aerospace companies introduce effective product-line engineering practices. He received the Premier's Research Excellence Award in 2004 and the British Computing Society in Upper Canada Award for Outstanding Contributions to IT Industry in 2008. He currently leads the NSERC CREATE in Product Line Engineering for Cyber-physical Systems, a $2.7 million industry-oriented graduate research and training program at the University of Waterloo.