Skip to main content
SpringerLink
Log in

A compositional semantics for fault-tolerant real-time systems

  • Session 1
  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1992)

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

Abstract

Motivated by the close relation between real-time and fault-tolerance, we investigate the foundations of a formal framework to specify and verify real-time distributed systems that incorporate fault-tolerance techniques. Therefore a denotational semantics is presented to describe the real-time behaviour of distributed programs in which concurrent processes communicate by synchronous message passing. New is that in this semantics we allow the occurrence of failures, due to faults of the underlying execution mechanism, and we describe the effect of these failures on the real-time behaviour of programs. Whenever appropriate we give alternative choices for the definition of the semantics. The main idea is that making only very weak assumptions about faults and their effect upon the behaviour of a program in the semantics, any hypothesis about faults must be made explicit in the correctness proof of a program.

Supported by NWO/SION Project 612-316-022: “Fault Tolerance: Paradigms, Models, Logics, Construction”.

Supported by ESPRIT-BRA Project 3096: “Formal Methods and Tools for the Development of Distributed Real-Time Systems (SPEC)”.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P.A. Bernstein. Sequoia: A Fault-Tolerant Tightly Coupled Multiprocessor for Transaction Processing. IEEE Computer pp. 37–46, February 1988.

    Google Scholar 

  2. J. Bartlett, J Gray & B. Horst. Fault Tolerance in Tandem Computer Systems. Symp. on the Evolution of Fault-Tolerant Computing, Baden, Austria, 1986.

    Google Scholar 

  3. F. Cristian, B. Dancey & J. Dehn. Fault-Tolerance in the Advanced Automation System. In “20th Annual Symp. on Fault-Tolerant Computing”, 1990.

    Google Scholar 

  4. F. Cristian. A Rigorous Approach to Fault-Tolerant Programming. IEEE Trans. on Softw. Engin.; SE-11(1):23–31, 1985.

    Google Scholar 

  5. H. Hansson & B. Jonsson. A Framework for Reasoning About Time and Reliability. Proc. 10th IEEE Real-Time Systems Symposium, pp. 101–111, 1989.

    Google Scholar 

  6. J. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.

    Google Scholar 

  7. J. Hooman & J. Widom. A Temporal-Logic Based Compositional Proof System for Real-Time Message Passing. Proc. PARLE '89 Vol. II:424–441; LNCS 366, 1989.

    Google Scholar 

  8. M. Joseph, A. Moitra & N. Soundararajan. Proof Rules for Fault Tolerant Distributed Programs. Science of Comp. Prog.; 8:43–67, 1987.

    Google Scholar 

  9. N. Kronenberg, H. Levy & W. Strecker. VAXclusters: A Closely-Coupled Distributed System. ACM Trans. on Computer Systems, 4:130–146, 1986.

    Google Scholar 

  10. INMOS Ltd. OCCAM 2 Reference Manual. Prentice-Hall, 1988.

    Google Scholar 

  11. J. Ostroff. Temporal Logic for Real-Time Systems. Advanced Software Development Series. Research Studies Press, 1989.

    Google Scholar 

  12. D. Powell, P. Verissimo, G. Bonn, F. Waeselynck & D. Seaton. The Delta-4 Approach to Dependability in Open Distributed Computing Systems. Proc. FTCS-18, IEEE Computer Society Press, 1988.

    Google Scholar 

  13. B. Randell, P.A. Lee & P.C. Treleaven. Reliability Issues in Computing System Design. ACM Computing Surveys, 10:123–165, 1978.

    Google Scholar 

  14. R.D. Schlichting & F.B. Schneider. Fail-stop processors: an approach to designing fault-tolerant computing systems. ACM Trans. on Comp. Sys.; 1(3):222–238, 1983.

    Google Scholar 

  15. A.U. Shankar & S.S. Lam. Time-Dependent Distributed Systems: Proving Safety, Liveness and Real-Time Properties. Distributed Computing; 2:61–79, 1987.

    Google Scholar 

  16. D. Taylor & G. Wilson. Stratus. In “Dependability of Resilient Computers”, T. Anderson Ed., Blackwell Scientific Publications, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    J. Coenen & J. Hooman

Authors
  1. J. Coenen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. Hooman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan Vytopil

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coenen, J., Hooman, J. (1991). A compositional semantics for fault-tolerant real-time systems. In: Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1992. Lecture Notes in Computer Science, vol 571. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55092-5_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-55092-5_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55092-1

  • Online ISBN: 978-3-540-46692-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation