Validating fault-tolerant behaviors of synchronous system specifications by discrete controller synthesis

We demonstrate the utility of discrete controller synthesis to formally assess the fault-tolerance capabilities of a dependable system from the early design stages. We start with an executable specification in order to yield a new fault-tolerant executable specification. Then, we obtain manually the final distributed implementation and we formally verify its conformity to the initial fault-tolerant specification.