Patrick Heymans et Pierre-Yves Schobbens, professeurs à la Faculté d’informatique, et leurs collègues se sont vus décerner le "Most Influential Paper Award" pour leur papier intitulé "Model checking lots of systems: efficient verification of temporal properties in software product lines". Les résultats de cette recherche ont été présentés à la conférence SPLC 2020 (ACM International Systems and Software Product Line Conference), qui s’est déroulée du 19 au 23 octobre 2020.
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.
