Skip to main content
SpringerLink
Log in
Book cover

International Conference on Parallel Architectures and Languages Europe

PARLE 1993: PARLE '93 Parallel Architectures and Languages Europe pp 197–208Cite as

Trace-based compositional reasoning about fault tolerant systems

  • Paper Sessions
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 694))

Abstract

In this report we present a compositional network proof theory to specify and verify safety properties of fault tolerant systems. Important in such systems is the fault hypothesis which specifies the class of faults that must be tolerated. In the formalism presented in this report, the fault hypothesis of a system is represented by a predicate which expresses how faults might transform the behaviour of the system. To reason about fault tolerant systems, we formulate a compositional proof method based on communication histories. Soundness and relative network completeness of the method is proven. Our approach is illustrated by applying it to the alternating bit protocol.

Supported by the Dutch NWO under grant number NWI88.1517: ‘Fault Tolerance: Paradigms, Models, Logics, Construction’.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Avižienis, A., Laprie, J.C.: Dependable Computing: From Concepts to Design Diversity, Proceedings of the IEEE 74(5) (May 1986) 629–638.

    Google Scholar 

  2. Bartlett, K.A, Scantlebury, R.A., Wilkinson, P.T.: A Note on Reliable Full-Duplex Transmission over Half-Duplex Links, CACM 12(5) (1969) 260–261.

    Google Scholar 

  3. Coenen, J., Hooman, J.: A Compositional Semantics for Fault Tolerant Real-Time Systems, Lecture Notes in Computer Science 571 (Springer, 1991) 33–51.

    Google Scholar 

  4. Cook, S.A.: Soundness and Completeness of an Axiom System for Program Verification, SIAM Journal on Computing 7(1) (February 1978) 70–90.

    Google Scholar 

  5. Cristian, F.: A Rigourous Approach to Fault Tolerant Programming, IEEE Trans. on Software Engineering SE-11(1) (1985) 23–31.

    Google Scholar 

  6. Hoare, C.A.R.: An Axiomatic Basis for Computer Programming, CACM 12(10) (1969) 576–580,583.

    Google Scholar 

  7. Hoare, C.A.R.: Communicating Sequential Processes (Prentice-Hall, 1985).

    Google Scholar 

  8. Hooman, J.: Specification and Compositional Verification of Real-Time Systems, Lecture Notes in Computer Science 558 (Springer, 1992).

    Google Scholar 

  9. Joseph, M., Moitra, A., Soundararajan, N.: Proof Rules for Fault Tolerant Distributed Programs, Science of Computer Programming 8 (1987) 43–67.

    Google Scholar 

  10. Lamport, L.: What Good is Temporal Logic, in: Manson, R.E., ed.: Information Processing (North-Holland, 1983) 657–668.

    Google Scholar 

  11. Laprie, J.C.: Dependable Computing and Fault Tolerance: Concepts and Terminology, Proc. 15th Int. Symp. on Fault Tolerant Computing Systems (IEEE Computer Society Press, 1985) 2–11.

    Google Scholar 

  12. Lee, P.A., Anderson, T.: Fault Tolerance: Principles and Practice (Springer, 1990).

    Google Scholar 

  13. Paliwoda, K., Sanders, J.W.: An Incremental Specification of the Sliding Window Protocol, Distributed Computing 5 (1991) 83–94.

    Google Scholar 

  14. Peleska, J.: Design and Verification of Fault Tolerant Systems with CSP, Distributed Computing 5 (1991) 95–106.

    Google Scholar 

  15. Randell, B., Lee, P.A., Treleaven, P.C.: Reliability Issues in Computing System Design, ACM Computing Surveys 10(2) (June 1978) 123–165.

    Google Scholar 

  16. Schepers, H.: Terminology and Paradigms for Fault Tolerance, in: Vytopil, J., ed.: Formal Techniques in Real-Time and Fault Tolerant Systems (Kluwer Academic Publishers, 1993) 3–31.

    Google Scholar 

  17. Schepers, H.: Tracing Fault Tolerance, Proc. 3rd IFIP Int. Working Conference on Dependable Computing for Critical Applications (to appear).

    Google Scholar 

  18. Schepers, H., Hooman, J.: A Trace-Based Compositional Proof Theory for Fault Tolerant Distributed Systems, Eindhoven University of Technology, 1993.

    Google Scholar 

  19. Weber, D.G.: Formal Specification of Fault-Tolerance and its Relation to Computer Security, ACM Software Engineering Notes 14(3) (1989) 273–277.

    Article  Google Scholar 

  20. Widom, J., Gries, D., Schneider, F.B.: Trace-based network proof systems: expressiveness and completeness, ACM TOPLAS 14(3) (July 1992) 396–416.

    Google Scholar 

  21. Zwiers, J.: Compositionality, Concurrency and Partial Correctness, Lecture Notes in Computer Science 321 (Springer, 1989).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB Eindhoven, The Netherlands

    Henk Schepers & Jozef Hooman

Authors
  1. Henk Schepers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jozef Hooman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Arndt Bode Mike Reeve Gottfried Wolf

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schepers, H., Hooman, J. (1993). Trace-based compositional reasoning about fault tolerant systems. In: Bode, A., Reeve, M., Wolf, G. (eds) PARLE '93 Parallel Architectures and Languages Europe. PARLE 1993. Lecture Notes in Computer Science, vol 694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56891-3_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-56891-3_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56891-9

  • Online ISBN: 978-3-540-47779-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation