Design and Verification of Fault-Tolerant Components

Miaomiao Zhang, Zhiming Liu, Anders Peter Ravn, Charles Morisset

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

12 Citationer (Scopus)

Abstrakt

We present a systematic approach to design and verification of fault-tolerant components with real-time properties as found in embedded systems. A state machine model of the correct component is augmented with internal transitions
that represent hypothesized faults. Also, constraints on the occurrence or timing of faults are included in this model. This model of a faulty component is then extended with fault detection and recovery mechanisms, again in the form of
state machines. Desired properties of the component are model checked for each of the successive models. The models can be made relatively detailed such that they can serve directly as blueprints for engineering, and yet be amenable to exhaustive verication. The approach is illustrated with a design of a triple modular fault-tolerant system that is a real case we received from our collaborators in the aerospace field. We use UPPAAL to model and check this design. Model checking uses concrete parameters, so we extend the result with parametric analysis using abstractions of the automata in a rigorous verification.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind5454
Sider (fra-til)57-84
Antal sider28
ISSN0302-9743
DOI
StatusUdgivet - 2009

Bibliografisk note

Titel:
Methods, Models and Tools for Fault Tolerance

Undertitel:
Methods, Models, and Tools for Fault Tolerance, State of the Art Survey

Oversat titel:


Oversat undertitel:


Forlag:
Springer

ISBN (Trykt):
978-3-642-00866-5

ISBN (Elektronisk):


Publikationsserier:
Lecture Notes in Computer Science, Springer, 0302-9743
Programming and Software Engineering, Springer, 5454

Redaktører:
Michael Butler
Cliff Jones
Alexander Romanovsky
Elena Troubitsyna

Fingeraftryk Dyk ned i forskningsemnerne om 'Design and Verification of Fault-Tolerant Components'. Sammen danner de et unikt fingeraftryk.

Citationsformater