Formal development of software for tolerating transient faults

Transient faults constitute a wide-spread class of faults typical in control systems. These are faults that appear for some time during system operation and might disappear and reappear later. However, even by appearing for a short time, they might cause dangerous system errors. Hence designing mechanisms for tolerating transient faults is an acute issue, especially in the development of safety-critical control systems. In this paper we propose a formal approach to specifying software-based mechanisms for tolerating transient faults in the B method. We focus on deriving a general specification and development pattern which can be applied in the development of various control systems. We illustrate an application of the proposed patterns by an example from avionics software product line.