Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F. Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. In: Journal of Logical and Algebraic Methods in Programming, vol. 85 (2) pp. 287 - 315. [Online first: 2015-11-30] Elsevier, 2016.
We present the formal underpinnings of a modelling and analysis framework for the specification and verification of variability in product families. We address variability at the behavioural level by modelling the family behaviour by means of a Modal Transition System (MTS) with an associated set of variability constraints expressed over action labels. An MTS is a Labelled Transition System (LTS) which distinguishes between optional and mandatory transitions. Steered by the variability constraints, the inclusion or exclusion of labelled transitions in an LTS refining the MTS determines the family's possible product behaviour. We formalise this as a special-purpose refinement relation for MTSs, which differs fundamentally from the classical one, and show how to use it for the definition and derivation of valid product behaviour starting from product family behaviour. We also present a variability-aware action-based branching-time modal temporal logic to express properties over MTSs, and demonstrate a number of results regarding the preservation of logical properties from family to product behaviour. These results pave the way for the more efficient family-based analyses of MTSs, limiting the need for product-by-product analyses of LTSs. Finally, we define a high-level modal process algebra for the specification of MTSs. The complete framework is implemented in a model-checking tool: given the behaviour of a product family modelled as an MTS with an additional set of variability constraints, it allows the explicit generation of valid product behaviour as well as the efficient on-the-fly verification of logical properties over family and product behaviour alike.
URL: http://www.sciencedirect.com/science/article/pii/S2352220815001431
DOI: 10.1016/j.jlamp.2015.11.006
Subject Model checking
Modal transition systems
Temporal logic
Product families
D.2.4 Software/Program Verification. Formal methods
D.2.4 Software/Program Verification. Model checking
D.2.13 Reusable Software. Domain engineering
F.3.2 Semantics of Programming Languages. Algebraic approaches to semantics
F.3.2 Semantics of Programming Languages. Process models
F.4.1 Mathematical Logic. Temporal logic

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional