Verifying families of system configurations

Electronics and computer science playa more and more prominent role in automotive technology. Likely, in the future, the prevalence of new technologies and the customers' demand for individuality will lead to a further increase in complexity and combinatorics of vehicle control systems. To cope with the resulting challenges in verification, new strategies need to be explored. One future challenge will be to determine a relatively small set of vehicle configurations, such that the successful verification of this set implies the correctness of the entire product family. This is especially important in the context of testing, where configurations are physically set up. Additionally, it can be relevant in the context of other verification techniques, such as formal verification, if those techniques are applied to individual configurations. This thesis presents an approach to address this challenge: locality set based configuration selection. Due to communalities between configurations, certain requirements do not need to be separately verified for each configuration. Particularly, requirements which describe functionality that is realized by the same subset of architectural elements, i. e., by the same locality set in different configurations, do not need to be repeatedly verified. We systematically exploit such communalities, in order to reduce the number of configurations that need to be set up in verification.