Design and Verification of a Fault-Tolerant System

 We present a design of a triple modular fault-tolerant system that is a real case we received from our collaborators in the aerospace field. The system is used to compute the action that a subsystem should take and output the result to another subsystem. We model the system as timed automata, where a fault is modelled as an unobservable transition from a "good state" to an "error state". Based on the faults that we were given by the application engineers, we design a system to tolerate the faults and use UPPAAL to check relevant properties. Keywords: Fault-tolerance, real-time embedded systems, abstraction techniques, model checking