Parametric Analysis of an Improved Fault Tolerant System

We report our preliminary study on an improved triple modular computer system from the aerospace field, which is designed to compute the course of action that other subsystems take and output the result to other subsystems. Based on the formal model of the system, we derive constraints on the values of the parameters that occur in our model, and manually prove that “ When a CPU is in the startup phase, it should not restart again due to its watchdog timer overflow or a restart signal sent from the arbitrator ”.