Design for Dependability
The concepts design, correctness of design, failure mode and fault tolerance are formally defined in terms of CSP. A systematic approach to verification of fault tolerance properties of designs is presented. The verification comprises a number of compositional proofs. It addresses safety and liveness properties of the design. As an example, a “cold stand by spare” fault tolerant design is formally defined and verified, using property oriented specifications of component failure assumptions and the compositional inference rules of CSP.
KeywordsFailure Mode Proof Rule Exception Signal Fault Tolerant System Incorrect Behaviour
Unable to display preview. Download preview PDF.
- F. Cristian. A rigorous approach to fault-tolerant programming. IEEE Transaction on Software Engineering, SE-11(1), 1985.Google Scholar
- C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
- J-C. Laprie. Dependable computing and fault tolerance: concepts and terminology. Proc. 15th International Symposium on Fault-tolerant Computing, IEEE, 1985.Google Scholar
- Z. Liu. Transformation of programs for fault tolerance. Formal Aspects of Computing, 4(5), 1992.Google Scholar
- L. V. Mancini, G. Pappalardo. Towards a theory of replicated processing. Proc. Symposium on Formal Techniques in Real-time and Fault Tolerant Systems (Lecture Notes in Computer Science 331), Springer Verlag, September 1988.Google Scholar
- J. Peleska. Design and verification of fault tolerant systems with csp. Distributed Computing, 5(2), 1991.Google Scholar
- J. P. Roth. Diagnosis of automata failures: a calculus and a method. IBM J. Res. Development, 10(4), 1966.Google Scholar
- F. B. Schneider. Implementing fault tolerant services using the state machine approach: a tutorial. ACM Computing Surveys, 22(5), 1990.Google Scholar