Istituto di Scienza e Tecnologie dell'Informazione     
Asirelli P., Ter Beek M., Fantechi A., Gnesi S. A logical framework to deal with variability. In: IFM 2010 - Integrated Formal Methods. 8th International Conference (Nancy, France, 11-14 Ottobre 2010). Proceedings, pp. 43 - 58. D. Méry, S. Merz (eds.). (Lecture Notes in Computer Science, vol. 6396). Springer, 2010.
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.
URL: http://www.springerlink.com/content/v2q5265t64v62u54/
DOI: 10.1007/978-3-642-16265-7_5
Subject Product family
Temporal logic
Deontic logic
D.2.1 Requirements/Specifications
D.2.4 Software/Program Verification
F.4.1 Mathematical 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