Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Formal Model-Driven Developmen...

Formal Model-Driven Development of Fault Tolerant Control Systems

Dubravka Ilic, Colin Snook, Elena Troubitsyna, Linas Laibinis, Formal Model-Driven Development of Fault Tolerant Control Systems. TUCS Technical Reports 828, Turku Centre for Computer Science, 2007.

Abstract:

Fault tolerance techniques aim at ensuring that a system continues to operate properly even in the presence of faults. Fault tolerance is especially important in safety-critical systems, where system failures might have catastrophic consequences. Transient faults – temporal defects within the system – are typical for control systems. However, they require complex mechanisms to tolerate them. In this paper, we propose an approach to formal model-driven development of Failure Management System (FMS) – a software component implementing a mechanism for tolerating transient faults in control systems in avionics. In our development we integrate formal modelling and verification in the B Method with graphical modelling in UML-B. UML-B is a specialized subset of UML which supports automatic translation of the subset of UML diagrams into the B specifications. By integrating formal and graphical modelling we combine benefits of visual modelling with rigorous verification. We develop generic patterns for modelling the FMS at different development stages starting at high level of abstraction till detailed pre-implementation specification. Correctness of model transformations is ensured by refinement relation. The developed generic patterns can be easily reused in the product line development in the avionics domain. Hence, the proposed approach facilitates reuse and leverages efficiency while ensuring dependability of developed systems.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tIlSnTrLa07a,
  title = {Formal Model-Driven Development of Fault Tolerant Control Systems},
  author = {Ilic, Dubravka and Snook, Colin and Troubitsyna, Elena and Laibinis, Linas},
  number = {828},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2007},
  keywords = {B Method, control systems, fault tolerance, refinement, transient faults, UML-B},
  ISBN = {978-952-12-1918-4},
}

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

Edit publication