Modeling Fault-tolerant Distributed Systems for Discrete Controller Synthesis

Embedded systems require safe design methods based on formal methods, as well as safe execution based on fault-tolerance techniques. We propose a safe design method for safe execution systems: it uses discrete controller synthesis (DCS) to generate a correct reconfiguring system. The properties enforced concern consistent execution, functionality fulfillment (whatever the faults, under some failure hypothesis), and several optimizations. We propose model patterns for a set of periodic tasks, a set of distributed, heterogeneous and fail-silent processors, and an environment model that expresses the potential fault patterns. We outline an implementation of our method, using the Sigali symbolic DCS tool and Mode Automata.