Trace-Based Compositional Refinement of Fault Tolerant Distributed Systems
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.
KeywordsFault Tolerant Safety Property Transmission Medium Acceptable Behaviour Weak Precondition
Unable to display preview. Download preview PDF.
- J. Hooman. Specification and Compositional Verification of Real-Time Systems. Lecture Notes in Computer Science 558 (Springer-Verlag, 1992).Google Scholar
- L. Lamport. What Good is Temporal Logic. In R.E. Manson (ed.). Information Processing (North-Holland, 1983) 657-668.Google Scholar
- E.R. Olderog. Nets, Terms, and Formulas. Cambridge Tracts in Computer Science 23 (Cambridge University Press, 1991).Google Scholar
- 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
- 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
- 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
- J. Zwiers. Compositionality, Concurrency and Partial Correctness. Lecture Notes in Computer Science 321 (Springer-Verlag, 1989).Google Scholar
- 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