Most Influential Paper Award SPLC 2020

Axel Legay, together with colleagues at the University of Namur, received the ICSE' 2020 Most Influential Paper (MIP) Award for their paper "Model checking lots of systems: efficient verification of temporal properties in software product lines”, by A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay and J.-F. Raskin.

The award was granted at SPLC 2020 (24th ACM International Systems and Software Product Line Conference), October 19-23, 2020.

The paper appeared in the ICSE'2010 Conference Proceedings. ICSE is the most prestigious international conference in software engineering, and the MIP+10 award is an annual award that recognizes the paper estimated to have had the most impact over a 10-year period since the paper was published.

This paper was the first to consider features at first-class citizens in modeling SPL behavior, resulting in the first rigorous account of behavioral variability and an associated rigorous family-based verification method.

This paper introduced the notion of a Featured Transition System (FTS) to the community, allowing scalable SPL modeling. Concretely, the authors extended labeled transition systems with features in order to concisely describe and analyze the combined behavior of a family of behavioral models. The paper also introduced dedicated family-based model-checking techniques that have enriched model-checking algorithms by offering a means to verify whether a property is satisfied by an FTS, in which case it is also satisfied by every product of the SPL, and if a property is violated, then the algorithm reports a counterexample as well as the products of the SPL that violate the property.

Overall, by carving out the right concept, this paper paved the way for a vast amount of research on formal analysis (testing, model checking, etc.) of variability in behavioral models of SPLs and configurable systems in general, and contributed to their dissemination in industrial settings. A number of SPL analysis tools nowadays accept FTSs as input format. In fact, FTSs have become the de-facto standard formalism for the formal analysis of behavior of models with variability.

^{Source : https://nouvelles.unamur.be/upnews.2020-11-23.4193802821/view}