We propose to use model checking to detect feature interactions in a set of features under design for an automotive embedded system. In this paper, we present (1) the characteristics of the feature interaction problem in the automotive domain that make model checking an appropriate detection technique; (2) our proposal for a general, systematic definition of feature interactions for this domain based on the set of actuators in the vehicle influenced by the features; and (3) our solutions to two modelling issues that arise when creating a description in SMV of the behaviour of an integrated set of automotive features designed in MATLAB's STATEFLOW.

The main goal of our research is to develop techniques for the detection of feature interactions for embedded systems in the automotive domain. Automotive systems are cyber-physical systems (CPS), which are composed of a "cyber" part that consists of software components running on digital hardware and a "physical" part that is the mechanical processes monitored by the software. Feature interactions in automotive systems arise from the activation of two or more features sending requests to the mechanical processes that create contradictory physical forces, possibly at distinct times, that cause unsafe behaviours. An example is having simultaneous requests to apply the brakes and the throttle. While both actions may be "correct" according to the intended behaviour of each feature, their interaction is undesired and potentially dangerous. To deal with the feature interaction problem, we propose to perform analysis at design time by using formal methods to detect all possible interactions.

Many distributed systems using IP-based communication protocols consist of chains of components that run concurrently and communicate asynchronously with their neighbours through ports. We present a compositional reasoning method using model checking and theorem proving to verify liveness properties of a communication protocol for chains of connections consisting of an unknown number of components. We outline how our method is used to verify properties of the call protocol of AT&T's Distributed Feature Composition (DFC) architecture.