Formal verification of fault-tolerant software design : the CSP approach

Wing Lok YEUNG, S. A. SCHNEIDER

Research output: Journal PublicationsJournal Article (refereed)Researchpeer-review

5 Citations (Scopus)

Abstract

Software design techniques for tolerating both hardware and software faults have been developed over the past few decades. Paradoxically, it is essential that fault-tolerant software is designed with the highest possible rigour to prevent faults in itself. Such rigour is provided by formal methods and aided by model checking. We illustrate an approach to fault-tolerant software design based on communicating sequential processes through a running example.
Original languageEnglish
Pages (from-to)197-209
Number of pages13
JournalMicroprocessors and Microsystems
Volume29
Issue number5
DOIs
Publication statusPublished - 1 Jun 2005

Fingerprint

Software design
Formal methods
Model checking
Hardware
Formal verification

Cite this

YEUNG, Wing Lok ; SCHNEIDER, S. A. / Formal verification of fault-tolerant software design : the CSP approach. In: Microprocessors and Microsystems. 2005 ; Vol. 29, No. 5. pp. 197-209.
@article{479830c0011e46c0979a32a739fe37d7,
title = "Formal verification of fault-tolerant software design : the CSP approach",
abstract = "Software design techniques for tolerating both hardware and software faults have been developed over the past few decades. Paradoxically, it is essential that fault-tolerant software is designed with the highest possible rigour to prevent faults in itself. Such rigour is provided by formal methods and aided by model checking. We illustrate an approach to fault-tolerant software design based on communicating sequential processes through a running example.",
author = "YEUNG, {Wing Lok} and SCHNEIDER, {S. A.}",
year = "2005",
month = "6",
day = "1",
doi = "10.1016/j.micpro.2004.07.005",
language = "English",
volume = "29",
pages = "197--209",
journal = "Microprocessors and Microsystems",
issn = "0141-9331",
publisher = "Elsevier",
number = "5",

}

Formal verification of fault-tolerant software design : the CSP approach. / YEUNG, Wing Lok; SCHNEIDER, S. A.

In: Microprocessors and Microsystems, Vol. 29, No. 5, 01.06.2005, p. 197-209.

Research output: Journal PublicationsJournal Article (refereed)Researchpeer-review

TY - JOUR

T1 - Formal verification of fault-tolerant software design : the CSP approach

AU - YEUNG, Wing Lok

AU - SCHNEIDER, S. A.

PY - 2005/6/1

Y1 - 2005/6/1

N2 - Software design techniques for tolerating both hardware and software faults have been developed over the past few decades. Paradoxically, it is essential that fault-tolerant software is designed with the highest possible rigour to prevent faults in itself. Such rigour is provided by formal methods and aided by model checking. We illustrate an approach to fault-tolerant software design based on communicating sequential processes through a running example.

AB - Software design techniques for tolerating both hardware and software faults have been developed over the past few decades. Paradoxically, it is essential that fault-tolerant software is designed with the highest possible rigour to prevent faults in itself. Such rigour is provided by formal methods and aided by model checking. We illustrate an approach to fault-tolerant software design based on communicating sequential processes through a running example.

UR - http://commons.ln.edu.hk/sw_master/2554

U2 - 10.1016/j.micpro.2004.07.005

DO - 10.1016/j.micpro.2004.07.005

M3 - Journal Article (refereed)

VL - 29

SP - 197

EP - 209

JO - Microprocessors and Microsystems

JF - Microprocessors and Microsystems

SN - 0141-9331

IS - 5

ER -