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

Wing Lok YEUNG; S. A. SCHNEIDER

doi:10.1016/j.micpro.2004.07.005

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

Wing Lok YEUNG, S. A. SCHNEIDER

Department of Computing and Decision Sciences

Research output: Journal Publications › Journal Article (refereed) › peer-review

6 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 language	English
Pages (from-to)	197-209
Number of pages	13
Journal	Microprocessors and Microsystems
Volume	29
Issue number	5
DOIs	https://doi.org/10.1016/j.micpro.2004.07.005
Publication status	Published - 1 Jun 2005

Bibliographical note

We would like to thank Iain Bate and the anonymous reviewers for their comments and suggestions. The first author would like to thank the staff and research students of the Formal Methods Group at Royal Holloway for their interesting and helpful discussion during his visit there when completing this work. The visit is supported by a study leave from Lingnan University, Hong Kong.

Keywords

Fault tolerance
Formal verification
Model checking
Software design

Access to Document

10.1016/j.micpro.2004.07.005

https://commons.ln.edu.hk/cgi/viewcontent.cgi?article=3555&context=sw_master

Cite this

@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.",

keywords = "Fault tolerance, Formal verification, Model checking, Software design",

author = "YEUNG, {Wing Lok} and SCHNEIDER, {S. A.}",

note = "We would like to thank Iain Bate and the anonymous reviewers for their comments and suggestions. The first author would like to thank the staff and research students of the Formal Methods Group at Royal Holloway for their interesting and helpful discussion during his visit there when completing this work. The visit is supported by a study leave from Lingnan University, Hong Kong.",

year = "2005",

month = jun,

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 B.V.",

number = "5",

}

TY - JOUR

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

AU - YEUNG, Wing Lok

AU - SCHNEIDER, S. A.

N1 - We would like to thank Iain Bate and the anonymous reviewers for their comments and suggestions. The first author would like to thank the staff and research students of the Formal Methods Group at Royal Holloway for their interesting and helpful discussion during his visit there when completing this work. The visit is supported by a study leave from Lingnan University, Hong Kong.

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.

KW - Fault tolerance

KW - Formal verification

KW - Model checking

KW - Software design

UR - http://www.scopus.com/inward/record.url?scp=18144374546&partnerID=8YFLogxK

U2 - 10.1016/j.micpro.2004.07.005

DO - 10.1016/j.micpro.2004.07.005

M3 - Journal Article (refereed)

SN - 0141-9331

VL - 29

SP - 197

EP - 209

JO - Microprocessors and Microsystems

JF - Microprocessors and Microsystems

IS - 5

ER -

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

Abstract

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this