2013
Contribution to book  Restricted

Families of dependable systems:a model checking approach

Gnesi S.

Model checking  Temporal logics  Product lines 

A number of models, logics and associated tools for the qualitative analysis of variability aspects and their use to deal with adaptability and evolvability of systems have recently been proposed. In these lectures, we will introduce the action-based branching-time temporal logic MHML which allows expressing constraints over the products of a family as well as constraints over their behaviour in a single logical framework. Based on model-checking techniques for MHML, a modelling and verification framework will be presented that can automatically generate all the valid productsof the family, visualise the family/products behaviour and efficiently model check properties expressed in MHML over products and families alike. The use of the above methods, techniques and tools will be applied to a scenario derived from a family of dependable systems.

Source: Engineering Dependable Software Systems, edited by Broy M., Peled D., Kalus G., pp. 115–140, 2013



Back to previous page
BibTeX entry
@inbook{oai:it.cnr:prodotti:277510,
	title = {Families of dependable systems:a model checking approach},
	author = {Gnesi S.},
	booktitle = {Engineering Dependable Software Systems, edited by Broy M., Peled D., Kalus G., pp. 115–140, 2013},
	year = {2013}
}
CNR ExploRA

Bibliographic record

Also available from

www.iospress.nlRestricted