11th Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES), pp. 100-109
In many embedded systems like in the automotive domain, safety-critical features are increasingly realized by software. Some of these features are often required to behave fail-operational, meaning that they must stay alive even in the presence of random hardware failures. In this paper, we introduce a constraint-based approach to calculate valid deployments of mixed critical software components to the execution nodes of a new fault-tolerant SW/HW architecture for electric vehicles. To avoid harm, faulty execution nodes have to be isolated from the remaining system. We treat the changes to the deployment that are required after isolations of execution nodes to keep those software components alive that realize fail-operational features. However, the remaining system resources may become insufficient to execute the full set of software components after such isolations. Hence, some components might have to be deactivated, meaning that features might get lost. Our approach allows to formally analyze which subset of features can still be provided after one or more isolations. We present an arithmetic system model of the deployment problem that can be solved by an SMT solver.