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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

5 Citationer (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.

Originalsprog	Engelsk
Titel	Proceedings of the 10th International Conference on Software Engineering and Applications
Redaktører	Pascal Lorenz, Leszek Maciaszek
Antal sider	10
Forlag	SciTePress
Publikationsdato	jul. 2015
Sider	219-228
ISBN (Elektronisk)	978-989-758-114-4
DOI	https://doi.org/10.5220/0005516402190228
Status	Udgivet - jul. 2015
Begivenhed	10th International Conference on Software Engineering and Applications - Colmar, Alsace, Frankrig Varighed: 22 jul. 2015 → 22 jul. 2015 Konferencens nummer: 10

Konference

Konference	10th International Conference on Software Engineering and Applications
Nummer	10
Land/Område	Frankrig
By	Colmar, Alsace
Periode	22/07/2015 → 22/07/2015

Adgang til dokumentet

10.5220/0005516402190228

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

http://10.5220/0005516402190228

INTREPID: INTelligent systems for Energy Prosumer buildIngs at District level
Larsen, K. G. (Projektdeltager), Skou, A. (Projektdeltager) & Ravn, A. P. (Projektdeltager)
FP7 STREP
01/11/2012 → 31/10/2015
Projekter: Projekt › Forskning
Totalflex
Skou, A. (Projektdeltager), Pedersen, T. B. (Projektdeltager), Bak-Jensen, B. (Projektdeltager), Kjeldskov, J. (Projektdeltager), Skov, M. B. (Projektdeltager) & Uhrenholt, R. W. (Projektdeltager)
ForskEL
01/01/2012 → 31/12/2016
Projekter: Projekt › Forskning

Citationsformater

@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",

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. i P Lorenz & L Maciaszek (red), Proceedings of the 10th International Conference on Software Engineering and Applications. SciTePress, s. 219-228, 10th International Conference on Software Engineering and Applications, Colmar, Alsace, Frankrig, 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. red. / Pascal Lorenz; Leszek Maciaszek. SciTePress, 2015. s. 219-228.

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › 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

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

Konference

Adgang til dokumentet

AUB Link

Andre filer og links

Fingeraftryk

Projekter

INTREPID: INTelligent systems for Energy Prosumer buildIngs at District level

Totalflex

Citationsformater