A Logical Framework to Deal with Variability

Abstract : We present a logical framework that is able to deal with variability in product family descriptions. The temporal logic MHML is based on the classical Hennessy{Milner logic with Until and we interpret it over Modal Transition Systems (MTSs). MTSs extend the classical notion of Labelled Transition Systems by distinguishing possible (may) and required (must) transitions: these two types of transitions are useful to describe variability in behavioural descriptions of product families. This leads to a novel deontic interpretation of the classical modal and temporal operators, which allows the expression of both constraints over the products of a family and constraints over their behaviour in a single logical framework. Finally, we sketch model-checking algorithms to verify MHML formulae as well as a way to derive correct products from a product family description.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.43-58, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00525109
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : lundi 11 octobre 2010 - 11:27:04
Dernière modification le : mercredi 4 octobre 2017 - 11:24:02

Identifiants

  • HAL Id : inria-00525109, version 1

Collections

Citation

Patrizia Asirelli, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi. A Logical Framework to Deal with Variability. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.43-58, 2010, Lecture Notes in Computer Science. 〈inria-00525109〉

Partager

Métriques

Consultations de la notice

21