Design and verification of distributed recovery blocks with CSP

Wing Lok YEUNG, S. A. SCHNEIDER

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

10 Citations (Scopus)

Abstract

A case study on the application of Communicating Sequential Processes (CSP) to the design and verification of fault-tolerant real-time systems is presented. The distributed recovery block (DRB) scheme is a desisn technique for the uniform treatment of hardware and software faults in real-time systems. Through a simple fault-tolerant real-time system design using the DRB scheme, the case study illustrates a paradigm for specifying fault-tolerant software and demonstrates how the different behavioural aspects of a fault-tolerant real-time system design can be separately and systematically specified, formulated, and verified using an integrated set of formal techniques based on CSP.
Original languageEnglish
Pages (from-to)225-248
Number of pages24
JournalFormal Methods in System Design
Volume22
Issue number3
DOIs
Publication statusPublished - 1 Jan 2003

Fingerprint

Real time systems
Fault-tolerant Systems
Recovery
Real-time
System Design
Systems analysis
Software
Fault-tolerant
Computer hardware
Fault
Paradigm
Hardware
Design
Demonstrate

Keywords

  • CSP
  • Distributed recovery block scheme
  • Fault-tolerance
  • Formal specification and verification
  • Real-time systems
  • Timewise refinement

Cite this

YEUNG, Wing Lok ; SCHNEIDER, S. A. / Design and verification of distributed recovery blocks with CSP. In: Formal Methods in System Design. 2003 ; Vol. 22, No. 3. pp. 225-248.
@article{6854b27339ad4d76be396b5c0a835c7c,
title = "Design and verification of distributed recovery blocks with CSP",
abstract = "A case study on the application of Communicating Sequential Processes (CSP) to the design and verification of fault-tolerant real-time systems is presented. The distributed recovery block (DRB) scheme is a desisn technique for the uniform treatment of hardware and software faults in real-time systems. Through a simple fault-tolerant real-time system design using the DRB scheme, the case study illustrates a paradigm for specifying fault-tolerant software and demonstrates how the different behavioural aspects of a fault-tolerant real-time system design can be separately and systematically specified, formulated, and verified using an integrated set of formal techniques based on CSP.",
keywords = "CSP, Distributed recovery block scheme, Fault-tolerance, Formal specification and verification, Real-time systems, Timewise refinement",
author = "YEUNG, {Wing Lok} and SCHNEIDER, {S. A.}",
year = "2003",
month = "1",
day = "1",
doi = "10.1023/A:1022997110855",
language = "English",
volume = "22",
pages = "225--248",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "3",

}

Design and verification of distributed recovery blocks with CSP. / YEUNG, Wing Lok; SCHNEIDER, S. A.

In: Formal Methods in System Design, Vol. 22, No. 3, 01.01.2003, p. 225-248.

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

TY - JOUR

T1 - Design and verification of distributed recovery blocks with CSP

AU - YEUNG, Wing Lok

AU - SCHNEIDER, S. A.

PY - 2003/1/1

Y1 - 2003/1/1

N2 - A case study on the application of Communicating Sequential Processes (CSP) to the design and verification of fault-tolerant real-time systems is presented. The distributed recovery block (DRB) scheme is a desisn technique for the uniform treatment of hardware and software faults in real-time systems. Through a simple fault-tolerant real-time system design using the DRB scheme, the case study illustrates a paradigm for specifying fault-tolerant software and demonstrates how the different behavioural aspects of a fault-tolerant real-time system design can be separately and systematically specified, formulated, and verified using an integrated set of formal techniques based on CSP.

AB - A case study on the application of Communicating Sequential Processes (CSP) to the design and verification of fault-tolerant real-time systems is presented. The distributed recovery block (DRB) scheme is a desisn technique for the uniform treatment of hardware and software faults in real-time systems. Through a simple fault-tolerant real-time system design using the DRB scheme, the case study illustrates a paradigm for specifying fault-tolerant software and demonstrates how the different behavioural aspects of a fault-tolerant real-time system design can be separately and systematically specified, formulated, and verified using an integrated set of formal techniques based on CSP.

KW - CSP

KW - Distributed recovery block scheme

KW - Fault-tolerance

KW - Formal specification and verification

KW - Real-time systems

KW - Timewise refinement

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

U2 - 10.1023/A:1022997110855

DO - 10.1023/A:1022997110855

M3 - Journal Article (refereed)

VL - 22

SP - 225

EP - 248

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

IS - 3

ER -