Abstract
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.
Supported in part by SERC research grants GR/F 57960 and GR/H 39499.
Preview
Unable to display preview. Download preview PDF.
References
R. H. Campbell, B. Randell, Error recovery in asynchronous systems, IEEE Transactions on Software Engineering, SE-12, 1986, 811–826.
K. M. Chandy, L. Lamport, Distributed snapshots: determining the global state of distributed systems, ACM Transaction on Computation Systems Vol. 3 (1985), 63–75.
K.M. Chandy, J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1989.
F. Cristian, A rigorous approach to fault tolerant programming, IEEE Transactions on Software Engineering, SE-11(1), 1985, 23–31.
G. Huet, B. Lang, Proving and applying program transformations expressed with second order patterns, Acta Informatica 11 (1978), 31–55.
R. Koo, S. Toueg, Checkpointing and rollback-recovery for distributed systems, IEEE Transactions on Software Engineering, SE-13, 1987, 23–31.
Z. Liu, M. Joseph, Transformations of programs for fault-tolerance, Formal Aspects of Computing, 4 (5), 1992, 442–469.
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.
D. Peled, M. Joseph, A Compositional Framework for Fault-Tolerance by Specification Transformation, submitted for publication.
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.
J. Zwiers, Compositionality, concurrency and partial correctness, Springer-Verlag, LNCS 321, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Peled, D., Joseph, M. (1993). A compositional approach for fault-tolerance using specification transformation. 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_14
Download citation
DOI: https://doi.org/10.1007/3-540-56891-3_14
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