Advertisement
Published in:
2010 | OriginalPaper | Chapter
A Logical Framework to Deal with Variability
Authors : Patrizia Asirelli, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi
Published in: Integrated Formal Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.