Implementing fault-tolerance in real-time systems by automatic program transformations

We present a formal approach to implement and certify fault-tolerance in real-time embedded systems. The faultintolerant initial system consists of a set of independent periodic tasks scheduled onto a set of fail-silent processors. We transform the tasks such that, assuming the availability of an additional spare processor, the system tolerates one failure at a time (transient or permanent). Failure detection is implemented using heartbeating, and failure masking using checkpointing and roll-back. These techniques are described and implemented by automatic program transformations on the tasks' programs. The proposed formal approach to faulttolerance by program transformation highlights the benefits of separation of concerns and allows us to establish correctness properties. Categories and Subject Descriptors C.3 [Computer Systems Organization]: Special-Purpose and Application-Based Systems, Real-time and embedded systems; D.4.5 [Software]: Operating Systems, Reliability [Checkpoi...

• Type: Conference
• Year: 2006
• Where: EMSOFT
• Authors: Tolga Ayav, Pascal Fradet, Alain Girault
• Keywords: Embedded Systems, EMSOFT 2006, Formal Approach, Program Transformations, Software Engineering