Trace-Based Compositional Refinement of Fault Tolerant Distributed Systems

  • Henk Schepers
  • Jos Coenen
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 9)


We present a trace-based compositional framework for the refinement of fault tolerant distributed systems. Important in such systems is the failure hypothesis that stipulates the class of failures that must be tolerated. In the formalism presented in this report, the failure hypothesis of a system is formalized as a relation between the system’s normal behaviour (i.e., the behaviour that conforms to the specification) and its acceptable behaviour, that is, the normal behaviour together with the exceptional behaviour (i.e., the behaviour whose abnormality should be tolerated). We highlight two aspects of refinement of fault tolerant distributed systems. First we show how to classify the system that under a particular failure hypothesis should satisfy a given specification. In the second place we determine the least stringent failure hypothesis such that a given system still satisfies a particular specification.


Fault Tolerant Safety Property Transmission Medium Acceptable Behaviour Weak Precondition 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    F. Cristian. Understanding Fault Tolerant Distributed Systems. Communications of the ACM 34(2) (1991) 56–78.CrossRefGoogle Scholar
  2. [2]
    C.A.R. Hoare. Communicating Sequential Processes. Communications of the ACM 21(8) (1978) 666–677.MathSciNetMATHCrossRefGoogle Scholar
  3. [3]
    J. Hooman. Specification and Compositional Verification of Real-Time Systems. Lecture Notes in Computer Science 558 (Springer-Verlag, 1992).Google Scholar
  4. [4]
    L. Lamport. What Good is Temporal Logic. In R.E. Manson (ed.). Information Processing (North-Holland, 1983) 657-668.Google Scholar
  5. [5]
    E.R. Olderog. Nets, Terms, and Formulas. Cambridge Tracts in Computer Science 23 (Cambridge University Press, 1991).Google Scholar
  6. [6]
    H. Schepers. Tracing Fault Tolerance. In Proc. 3rd IFIP Int. Working Conference on Dependable Computing for Critical Applications, Dependable Computing and Fault Tolerant Systems 8 (Springer-Verlag, 1993) 91–110.Google Scholar
  7. [7]
    H. Schepers and R. Gerth. A Compositional Proof Theory for Fault Tolerant Real-Time Distributed Systems. In Proc. 12th Symp. on Reliable Distributed Systems (IEEE Computer Society Press, 1993) 34-43.Google Scholar
  8. [8]
    H. Schepers and J. Hooman. A Trace-Based Compositional Proof Theory for Fault Tolerant Distributed Systems. Eindhoven University of Technology, 1993. To appear in Theoretical Computer Science; an extended abstract appeared in Proc. Parallel Architectures and Languages Europe (PARLE) ’93, Lecture Notes in Computer Science 694 (Springer-Verlag, 1993) 197-208.Google Scholar
  9. [9]
    J. Zwiers. Compositionality, Concurrency and Partial Correctness. Lecture Notes in Computer Science 321 (Springer-Verlag, 1989).Google Scholar
  10. [10]
    J. Zwiers, J. Coenen, and W.-P. de Roever. A Note on Compositional Refinement. In Proc. 5th BCS-FACS Refinement Workshop, 5th Refinement Workshop (Springer-Verlag, 1992) 342-366.Google Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Henk Schepers
    • 1
  • Jos Coenen
    • 2
  1. 1.Specification, Design & Realisation DepartmentPhilips Research Laboratories, Information & Software TechnologyEindhovenThe Netherlands
  2. 2.Department of Mathematics and Computing ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations