Translating Models of Automotive Features in MATLAB’s Stateflow to SMV to Detect Feature Interactions

Feature interactions are becoming more prevalent as systems increase in complexity, and can be a source of significant risk. When features that are designed to run independently are integrated within a system, the combination of their behaviours may interfere with each other. We propose to use the formal verification technique of symbolic model checking to examine exhaustively all behaviours of an integrated set of features to detect feature interactions. In this paper, we describe how to translate automotive features described in MATLAB's Stateflow language into the input language of the model checker SMV. MATLAB's Stateflow is used extensively for designing embedded components in various domains such as the automotive and avionics industries. SMV has powerful features for model checking and has a flexible input language, in which we can describe the semantics of Stateflow and of the composition of features. The translated SMV models contain the same level of description as the design, so that the findings of our analysis can be directly understood in terms of the feature design in Stateflow