A Method for Model Checking Feature Interactions

Thomas Pedersen; Thibaut Le Guilly; Anders Peter Ravn; Arne Joachim Skou

doi:10.5220/0005516402190228

A Method for Model Checking Feature Interactions

Thomas Pedersen, Thibaut Le Guilly, Anders Peter Ravn, Arne Joachim Skou

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

5 Citations (Scopus)

Abstract

This paper presents a method to check for feature interactions in a system assembled from independently developed concurrent processes as found in many reactive systems. The method combines and refines existing definitions and adds a set of activities. The activities describe how to populate the definitions with models to ensure that all interactions are captured. The method is illustrated on a home automation example with model checking as analysis tool. In particular, the modelling formalism is timed automata and the analysis uses UPPAAL to find interactions.

Original language	English
Title of host publication	Proceedings of the 10th International Conference on Software Engineering and Applications
Editors	Pascal Lorenz, Leszek Maciaszek
Number of pages	10
Publisher	SCITEPRESS Digital Library
Publication date	Jul 2015
Pages	219-228
ISBN (Electronic)	978-989-758-114-4
DOIs	https://doi.org/10.5220/0005516402190228
Publication status	Published - Jul 2015
Event	10th International Conference on Software Engineering and Applications - Colmar, Alsace, France Duration: 22 Jul 2015 → 22 Jul 2015 Conference number: 10

Conference

Conference	10th International Conference on Software Engineering and Applications
Number	10
Country/Territory	France
City	Colmar, Alsace
Period	22/07/2015 → 22/07/2015

Keywords

Feature Interaction
Control Systems
Model-driven Development
Home Automation
Model Checking
Timed Automata

Access to Document

10.5220/0005516402190228

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{48db7a16cf8f449e93231b5a10148df3,

title = "A Method for Model Checking Feature Interactions",

abstract = "This paper presents a method to check for feature interactions in a system assembled from independently developed concurrent processes as found in many reactive systems. The method combines and refines existing definitions and adds a set of activities. The activities describe how to populate the definitions with models to ensure that all interactions are captured. The method is illustrated on a home automation example with model checking as analysis tool. In particular, the modelling formalism is timed automata and the analysis uses UPPAAL to find interactions.",

keywords = "Feature Interaction, Control Systems, Model-driven Development, Home Automation, Model Checking, Timed Automata ",

author = "Thomas Pedersen and {Le Guilly}, Thibaut and Ravn, {Anders Peter} and Skou, {Arne Joachim}",

year = "2015",

month = jul,

doi = "10.5220/0005516402190228",

language = "English",

pages = "219--228",

editor = "Pascal Lorenz and Leszek Maciaszek",

booktitle = "Proceedings of the 10th International Conference on Software Engineering and Applications",

publisher = "SCITEPRESS Digital Library",

note = "10th International Conference on Software Engineering and Applications, ICSOFT-EA 2015 ; Conference date: 22-07-2015 Through 22-07-2015",

}

Pedersen, T, Le Guilly, T, Ravn, AP & Skou, AJ 2015, A Method for Model Checking Feature Interactions. in P Lorenz & L Maciaszek (eds), Proceedings of the 10th International Conference on Software Engineering and Applications. SCITEPRESS Digital Library, pp. 219-228, 10th International Conference on Software Engineering and Applications, Colmar, Alsace, France, 22/07/2015. https://doi.org/10.5220/0005516402190228

A Method for Model Checking Feature Interactions. / Pedersen, Thomas; Le Guilly, Thibaut; Ravn, Anders Peter et al.
Proceedings of the 10th International Conference on Software Engineering and Applications. ed. / Pascal Lorenz; Leszek Maciaszek. SCITEPRESS Digital Library, 2015. p. 219-228.

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - A Method for Model Checking Feature Interactions

AU - Pedersen, Thomas

AU - Le Guilly, Thibaut

AU - Ravn, Anders Peter

AU - Skou, Arne Joachim

N1 - Conference code: 10

PY - 2015/7

Y1 - 2015/7

N2 - This paper presents a method to check for feature interactions in a system assembled from independently developed concurrent processes as found in many reactive systems. The method combines and refines existing definitions and adds a set of activities. The activities describe how to populate the definitions with models to ensure that all interactions are captured. The method is illustrated on a home automation example with model checking as analysis tool. In particular, the modelling formalism is timed automata and the analysis uses UPPAAL to find interactions.

AB - This paper presents a method to check for feature interactions in a system assembled from independently developed concurrent processes as found in many reactive systems. The method combines and refines existing definitions and adds a set of activities. The activities describe how to populate the definitions with models to ensure that all interactions are captured. The method is illustrated on a home automation example with model checking as analysis tool. In particular, the modelling formalism is timed automata and the analysis uses UPPAAL to find interactions.

KW - Feature Interaction

KW - Control Systems

KW - Model-driven Development

KW - Home Automation

KW - Model Checking

KW - Timed Automata

UR - http://10.5220/0005516402190228

U2 - 10.5220/0005516402190228

DO - 10.5220/0005516402190228

M3 - Article in proceeding

SP - 219

EP - 228

BT - Proceedings of the 10th International Conference on Software Engineering and Applications

A2 - Lorenz, Pascal

A2 - Maciaszek, Leszek

PB - SCITEPRESS Digital Library

T2 - 10th International Conference on Software Engineering and Applications

Y2 - 22 July 2015 through 22 July 2015

ER -

A Method for Model Checking Feature Interactions

Abstract

Conference

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

INTREPID: INTelligent systems for Energy Prosumer buildIngs at District level

Totalflex

Cite this

A Method for Model Checking Feature Interactions

Abstract

Conference

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Projects

INTREPID: INTelligent systems for Energy Prosumer buildIngs at District level

Totalflex

Cite this