High-Level Modelling and Formal Semantics of Product-Line Behaviour

  • Arno Jeanjot

Thèse de l'étudiant: Master typesMaster en sciences informatiques


Software Product Line (SPL) methods have become more and more popular. They have been applied on several domains including critical systems which require quality assurance techniques in order to avoid error. An established quality assurance technique is model checking that verifies if a system under certain consideration holds certain properties. However, an SPL may potentially be compound of thousands
of products and verify each product of a line at a time would be suboptimal. To avoid this problem, there is a formalism called Featured Transition System (FTS) that allows merging the behaviour of every product of a line in a single model and verifying this model by using algorithms specially defined for this formalism.
Unfortunately, model checking techniques are not popular in industry. Indeed, FTS has its own language that requires some expertise to be fully understandable. This thesis aims to bridge the gap between FTS model checking and the industry by defining a variability-aware extension of a state-based language
commonly used in industry. The semantics of this extension will be defined in terms of FTS which allow the use FTS model checking techniques on systems modelled in this language.
la date de réponse4 sept. 2013
langue originaleAnglais
L'institution diplômante
  • Universite de Namur
SuperviseurPIERRE-YVES SCHOBBENS (Promoteur) & MAXIME CORDY (Copromoteur)

Contient cette citation