Where academic tradition
meets the exciting future

Formal Development of Mechanisms for Tolerating Transient Faults

Dubravka Ilic, Elena Troubitsyna, Linas Laibinis, Colin Snook, Formal Development of Mechanisms for Tolerating Transient Faults. TUCS Technical Reports 763, Turku Centre for Computer Science, 2006.

Abstract:

Transient faults belong to a wide-spread class of faults typical in control systems. These
are faults that appear for a short period of time and might reappear later. However, even
by appearing for a short time, they might cause dangerous system errors. Hence,
designing mechanisms for tolerating and recovering from transient faults is an acute
issue, especially in the development of safety-critical control systems. In this paper we propose a formal development (based on the B Method) of a software-based
mechanisms for tolerating transient faults. The mechanism relies on a specific
architecture of error detection actions called evaluating tests. These tests are executed
(with different frequencies) on predefined subsets of analyzed data. Our formal model
allows us to formally express and verify interdependencies between tests as well as to
define the test scheduling. Application of the proposed approach ensures proper damage
confinement caused by transient faults. We use our approach in the avionics domain,
focusing on a formal development of the engine Failure Management System. The
proposed specification and refinement patterns can be applied in the development of
control systems in other application domains as well.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tIlTrLaSn06a,
  title = {Formal Development of Mechanisms for Tolerating Transient Faults},
  author = {Ilic, Dubravka and Troubitsyna, Elena and Laibinis, Linas and Snook, Colin},
  number = {763},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2006},
  ISBN = {952-12-1709-X},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication