A Fault-Tolerant Software Architecture and its Formal Specification for Embedded, Real-Time Interactive Systems

International audienceMost of the work that has been done to build reliable interactive systems has been focusing on avoiding the occurrence of faults during the development of the system, using for instance formal verification techniques. However, empirical studies have demonstrated that software crashes may occur at runtime, even if the development has been extremely rigorous. One of the many sources of such crashes is called natural faults triggered by alpha-particles from radioactive contaminants in the chips or neutron from cosmic radiation. A higher probability of occurrence of faults concerns systems deployed in the high atmosphere (e.g. aircrafts) or in space (e.g. manned spacecraft). Therefore mechanisms are needed to deal with these faults and guarantee that the system will work correctly even in the presence of these faults. To deal with this issue, this paper proposes a fault-tolerant software architecture and its formal specification applied to embedded, real-time interactive systems