Title

Design and verification of distributed recovery blocks with CSP

Document Type

Journal article

Source Publication

Formal Methods in System Design

Publication Date

1-1-2003

Volume

22

Issue

3

First Page

225

Last Page

248

Keywords

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

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.

DOI

10.1023/A:1022997110855

Print ISSN

09259856

E-ISSN

15728102

Publisher Statement

Copyright © 2003 Kluwer Academic Publishers

Access to external full text or publisher's version may require subscription.

Full-text Version

Publisher’s Version

Recommended Citation

Yeung, W. L., & Schneider, S. A. (2003). Design and verification of distributed recovery blocks with CSP. Formal Methods in System Design, 22(3), 225-248. doi: 10.1023/A:1022997110855