Abstract
The fault tolerance theories by Arora and Kulkarni [3] and by Jhumka et al. [8] view a fault-tolerant program as the composition of a fault-intolerant program with fault tolerance components called detectors and correctors. At their core, the theories assume that the correctness specifications under consideration are fusion closed. In general, fusion closure of specifications can be achieved by adding history variables. However, the addition of history variables causes an exponential growth of the state space of the program, causing addition of fault tolerance to be expensive. To redress this problem, we present a method which can be used to add history information to a program in a way that significantly reduces the number of additional states. Hence, automated methods that add fault tolerance can be efficiently applied in environments where specifications are not necessarily fusion closed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
Arora, A., Kulkarni, S.S.: Component based design of multitolerant systems. IEEE Transactions on Software Engineering 24(1), 63–78 (1998)
Cau, A., de Roever, W.-P.: Specifying fault tolerance within stark’s formalism. In: Laprie, J.-C. (ed.) Proceedings of the 23rd Annual International Symposium on Fault-Tolerant Computing (FTCS 1993), Toulouse, France, June 1993, pp. 392–401. IEEE Computer Society Press, Los Alamitos (1993)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Gärtner, F.C., Jhumka, A.: Automating the addition of fail-safe fault-tolerance: Beyond fusion-closed specifications. Technical Report IC/2003/23, Swiss Federal Institute of Technology (EPFL), School of Computer and Communication Sciences, Lausanne, Switzerland (April 2003)
Gumm, H.P.: Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. Information Processing Letters 47(6), 291–294 (1993)
Jhumka, A., Gärtner, F.C., Fetzer, C., Suri, N.: On systematic design of fast and perfect detectors. Technical Report 200263, Swiss Federal Institute of Technology (EPFL), School of Computer and Communication Sciences, Lausanne, Switzerland (September 2002)
Kulkarni, S.S., Arora, A.: Automating the addition of fault-tolerance. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 82–93. Springer, Heidelberg (2000)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)
Liu, Z., Joseph, M.: Specification and verification of fault-tolerance, timing and scheduling. ACM Transactions on Programming Languages and Systems 21(1), 46–89 (1999)
Mantel, H., Gärtner, F.C.: A case study in the mechanical verification of fault tolerance. Journal of Experimental & Theoretical Artificial Intelligence (JETAI) 12(4), 473–488 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gärtner, F.C., Jhumka, A. (2004). Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications. In: Lakhnech, Y., Yovine, S. (eds) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. FTRTFT FORMATS 2004 2004. Lecture Notes in Computer Science, vol 3253. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30206-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-30206-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23167-7
Online ISBN: 978-3-540-30206-3
eBook Packages: Springer Book Archive