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 language | English |
|---|---|
| Pages (from-to) | 225-248 |
| Number of pages | 24 |
| Journal | Formal Methods in System Design |
| Volume | 22 |
| Issue number | 3 |
| DOIs | |
| Publication status | Published - 1 Jan 2003 |
Funding
The authors are also grateful to the British Council for a travel grant under the UK/Hong Kong Joint Research Scheme which has supported this work. The second author is grateful for DERA for supporting this work.
Keywords
- CSP
- Distributed recovery block scheme
- Fault-tolerance
- Formal specification and verification
- Real-time systems
- Timewise refinement