Design and verification of distributed recovery blocks with CSP
Yeung, WL and Schneider, SA (2003) Design and verification of distributed recovery blocks with CSP FORM METHOD SYST DES, 22 (3). 225 - 248. ISSN 0925-9856
| PDF 288Kb |
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 design 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.
| Item Type: | Article |
|---|---|
| Additional Information: | This is a pre-press version of an article published in Formal Methods in System Design, 22, 225-248. Click here to access the published version. © 2003 Springer. |
| Uncontrolled Keywords: | real-time systems, fault-tolerance, distributed recovery block scheme, CSP, formal specification and verification, timewise refinement, COMMUNICATING SEQUENTIAL PROCESSES, FAULT-TOLERANT ARCHITECTURES, SOFTWARE, HARDWARE, SYSTEMS |
| Divisions: | Faculty of Engineering and Physical Sciences > Computing Science |
| ID Code: | 1881 |
| Deposited By: | Mr Adam Field |
| Deposited On: | 27 May 2010 15:45 |
| Last Modified: | 26 Sep 2012 14:37 |
Document Downloads
Repository Staff Only: item control page
Tools
Tools