Abstract
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.
This research was supported through NWO project ‘Fault Tolerance: Paradigms, Models, Logics, Construction’ under STW grant number NWI88.1517 and SION grant number 612-316-103.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
F. Cristian. Understanding Fault Tolerant Distributed Systems. Communications of the ACM 34(2) (1991) 56–78.
C.A.R. Hoare. Communicating Sequential Processes. Communications of the ACM 21(8) (1978) 666–677.
J. Hooman. Specification and Compositional Verification of Real-Time Systems. Lecture Notes in Computer Science 558 (Springer-Verlag, 1992).
L. Lamport. What Good is Temporal Logic. In R.E. Manson (ed.). Information Processing (North-Holland, 1983) 657-668.
E.R. Olderog. Nets, Terms, and Formulas. Cambridge Tracts in Computer Science 23 (Cambridge University Press, 1991).
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.
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.
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.
J. Zwiers. Compositionality, Concurrency and Partial Correctness. Lecture Notes in Computer Science 321 (Springer-Verlag, 1989).
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Springer-Verlag/Wien
About this paper
Cite this paper
Schepers, H., Coenen, J. (1995). Trace-Based Compositional Refinement of Fault Tolerant Distributed Systems. In: Cristian, F., Le Lann, G., Lunt, T. (eds) Dependable Computing for Critical Applications 4. Dependable Computing and Fault-Tolerant Systems, vol 9. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9396-9_25
Download citation
DOI: https://doi.org/10.1007/978-3-7091-9396-9_25
Publisher Name: Springer, Vienna
Print ISBN: 978-3-7091-9398-3
Online ISBN: 978-3-7091-9396-9
eBook Packages: Springer Book Archive