A compositional approach for fault-tolerance using specification transformation
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.
KeywordsGlobal State Linear Temporal Logic Basic Program Execution Sequence Formula Transformation
Unable to display preview. Download preview PDF.
- R. H. Campbell, B. Randell, Error recovery in asynchronous systems, IEEE Transactions on Software Engineering, SE-12, 1986, 811–826.Google Scholar
- 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
- K.M. Chandy, J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1989.Google Scholar
- F. Cristian, A rigorous approach to fault tolerant programming, IEEE Transactions on Software Engineering, SE-11(1), 1985, 23–31.Google Scholar
- R. Koo, S. Toueg, Checkpointing and rollback-recovery for distributed systems, IEEE Transactions on Software Engineering, SE-13, 1987, 23–31.Google Scholar
- Z. Liu, M. Joseph, Transformations of programs for fault-tolerance, Formal Aspects of Computing, 4 (5), 1992, 442–469.Google Scholar
- 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
- D. Peled, M. Joseph, A Compositional Framework for Fault-Tolerance by Specification Transformation, submitted for publication.Google Scholar
- 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
- J. Zwiers, Compositionality, concurrency and partial correctness, Springer-Verlag, LNCS 321, 1987.Google Scholar