A Method for Model Checking Feature Interactions

Publication: Research - peer-reviewArticle in proceeding

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.
Close

Details

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 languageEnglish
Title of host publicationProceedings of the 10th International Conference on Software Engineering and Applications
EditorsPascal Lorenz, Leszek Maciaszek
Number of pages10
PublisherSCITEPRESS Digital Library
Publication dateJul 2015
Pages219-228
ISBN (electronic)978-989-758-114-4
DOI
StatePublished - Jul 2015
Event10th International Conference on Software Engineering and Applications - Colmar, Alsace, France

Conference

Conference10th International Conference on Software Engineering and Applications
Nummer10
LandFrance
ByColmar, Alsace
Periode22/07/201522/07/2015

    Keywords

  • Feature Interaction, Control Systems, Model-driven Development, Home Automation, Model Checking, Timed Automata
ID: 217797805