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

  • Arno Jeanjot

Student thesis: Master typesMaster in Computer science

Abstract

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.
Date of Award4 Sep 2013
Original languageEnglish
Awarding Institution
  • University of Namur
SupervisorPIERRE-YVES SCHOBBENS (Supervisor) & MAXIME CORDY (Co-Supervisor)

Cite this

High-Level Modelling and Formal Semantics of Product-Line Behaviour
Jeanjot, A. (Author). 4 Sep 2013

Student thesis: Master typesMaster in Computer science