Design and verification of distributed recovery blocks with CSP
Formal Methods in System Design
CSP, Distributed recovery block scheme, Fault-tolerance, Formal specification and verification, Real-time systems, Timewise refinement
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.
Copyright © 2003 Kluwer Academic Publishers
Access to external full text or publisher's version may require subscription.
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