Design and verification of distributed recovery blocks with CSP

Wing Lok YEUNG, S. A. SCHNEIDER

Research output: Journal PublicationsJournal Article (refereed)

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

Keywords

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

Cite this