Using model-checking for the detection of non-functional feature interactions

Systems integrated of many components often produce unforeseen or unexpected behaviour, so-called feature interactions. These effects can have many different causes, depending on both functional- or non-functional properties. In this paper we focus on non-functional feature interactions which occur due non-functional properties like resource usage. Our approach is to create a coarse-grained, abstract model of sufficiently low complexity which permits model-checking of non-functional properties. The automatically generated failure traces need to be cross-checked using a more detailed, executable model or implementation. In this way we can detect critical cases on the abstract models. The approach is validated with two examples from the automotive domain using timed automata which model the non-functional properties.