Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F.
Modal transition systems Computational Theory and Mathematics Variability Theoretical Computer Science Model checking Product families Software Logic Temporal logic
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.
Source: Journal of Logical and Algebraic Methods in Programming [online] 85 (2016): 287–315. doi:10.1016/j.jlamp.2015.11.006
Publisher: Elsevier, Amsterdam, NH.
@article{oai:it.cnr:prodotti:344828, title = {Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints}, author = {Ter Beek M. H. and Fantechi A. and Gnesi S. and Mazzanti F.}, publisher = {Elsevier, Amsterdam, NH.}, doi = {10.1016/j.jlamp.2015.11.006}, journal = {Journal of Logical and Algebraic Methods in Programming [online]}, volume = {85}, pages = {287–315}, year = {2016} }
A Decade of Featured Transition Systems
Bridging the Gap Between Supervisory Control and Coordination of Services: Synthesis of Orchestrations and Choreographies
States and Events in KandISTI
Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
The Legacy of Stefania Gnesi
Variability Modelling and Analysis During 30 Years