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