Advertisement

Design for Dependability

  • Jens Nordahl
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 8)

Abstract

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.

Keywords

Failure Mode Proof Rule Exception Signal Fault Tolerant System Incorrect Behaviour 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    F. Cristian. A rigorous approach to fault-tolerant programming. IEEE Transaction on Software Engineering, SE-11(1), 1985.Google Scholar
  2. [2]
    C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
  3. [3]
    J-C. Laprie. Dependable computing and fault tolerance: concepts and terminology. Proc. 15th International Symposium on Fault-tolerant Computing, IEEE, 1985.Google Scholar
  4. [4]
    Z. Liu. Transformation of programs for fault tolerance. Formal Aspects of Computing, 4(5), 1992.Google Scholar
  5. [5]
    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
  6. [6]
    J. Peleska. Design and verification of fault tolerant systems with csp. Distributed Computing, 5(2), 1991.Google Scholar
  7. [7]
    J. P. Roth. Diagnosis of automata failures: a calculus and a method. IBM J. Res. Development, 10(4), 1966.Google Scholar
  8. [8]
    F. B. Schneider. Implementing fault tolerant services using the state machine approach: a tutorial. ACM Computing Surveys, 22(5), 1990.Google Scholar

Copyright information

© Springer-Verlag Wien 1993

Authors and Affiliations

  • Jens Nordahl
    • 1
  1. 1.Department of Computer ScienceTechnical University of DenmarkLyngbyDenmark

Personalised recommendations