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
Language
English
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
