A compositional approach for fault-tolerance using specification transformation

  • Doron Peled
  • Mathai Joseph
Paper Sessions Concurrency: Responsive Systems
Part of the Lecture Notes in Computer Science book series (LNCS, volume 694)


The incorporation of a recovery algorithm into a program can be viewed as a program transformation, converting the basic program into a fault-tolerant version. We present a framework in which such program transformations are accompanied by a corresponding formula transformation which obtains properties of the fault-tolerant versions of the programs from properties of the basic programs. Compositionality is achieved when every property of the fault-tolerant version can be obtained from a transformed property of the basic program.

A verification method for proving the correctness of formula transformations is presented. This makes it possible to prove just once that a formula transformation corresponds to a program transformation, removing the need to prove separately the correctness of each transformed program.


Global State Linear Temporal Logic Basic Program Execution Sequence Formula Transformation 
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]
    R. H. Campbell, B. Randell, Error recovery in asynchronous systems, IEEE Transactions on Software Engineering, SE-12, 1986, 811–826.Google Scholar
  2. [2]
    K. M. Chandy, L. Lamport, Distributed snapshots: determining the global state of distributed systems, ACM Transaction on Computation Systems Vol. 3 (1985), 63–75.Google Scholar
  3. [3]
    K.M. Chandy, J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1989.Google Scholar
  4. [4]
    F. Cristian, A rigorous approach to fault tolerant programming, IEEE Transactions on Software Engineering, SE-11(1), 1985, 23–31.Google Scholar
  5. [5]
    G. Huet, B. Lang, Proving and applying program transformations expressed with second order patterns, Acta Informatica 11 (1978), 31–55.CrossRefGoogle Scholar
  6. [6]
    R. Koo, S. Toueg, Checkpointing and rollback-recovery for distributed systems, IEEE Transactions on Software Engineering, SE-13, 1987, 23–31.Google Scholar
  7. [7]
    Z. Liu, M. Joseph, Transformations of programs for fault-tolerance, Formal Aspects of Computing, 4 (5), 1992, 442–469.Google Scholar
  8. [8]
    Z. Manna, A. Pnueli, How to cook a temporal proof system for your pet language. Proc. ACM Symposium on Principles on Programming Languages, 1983, 141–151.Google Scholar
  9. [9]
    D. Peled, M. Joseph, A Compositional Framework for Fault-Tolerance by Specification Transformation, submitted for publication.Google Scholar
  10. [10]
    R. D. Schlichting, F. B. Schneider, Fail-stop processors: an approach to designing fault-tolerant computing systems, ACM Transactions on Computer Systems, 1, 1983, 222–238.Google Scholar
  11. [11]
    J. Zwiers, Compositionality, concurrency and partial correctness, Springer-Verlag, LNCS 321, 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Doron Peled
    • 1
  • Mathai Joseph
    • 2
  1. 1.AT&T Bell LaboratoriesMurray HillUSA
  2. 2.Department of Computer ScienceUniversity of WarwickCoventryUK

Personalised recommendations