Abstract
Self-stabilization is an elegant way of realizing non-masking fault-tolerant systems. Sustained research over last decades has produced multiple self-stabilizing algorithms for many problems in distributed computing. In this paper, we present a framework to evaluate multiple self-stabilizing solutions under a fault model that allows intermittent transient faults. To that end, metrics to quantify the dependability of self-stabilizing systems are defined. It is also shown how to derive models that are suitable for probabilistic model checking in order to determine those dependability metrics. A heuristics-based method is presented to analyze counterexamples returned by a probabilistic model checker in case the system under investigation does not exhibit the desired degree of dependability. Based on the analysis, the self-stabilizing algorithm is subsequently refined.
This work was supported by the German Research Foundation (DFG) under grant SFB/TR 14/2 “AVACS,” www.avacs.org
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
Dhama, A., Theel, O., Warns, T.: Reliability and Availability Analysis of Self-Stabilizing Systems. In: Datta, A.K., Gradinariu, M. (eds.) SSS 2006. LNCS, vol. 4280, pp. 244–261. Springer, Heidelberg (2006)
Arora, A., Kulkarni, S.S.: Component Based Design of Multitolerant Systems. IEEE Trans. Software Eng. 24, 63–78 (1998)
Arora, A., Kulkarni, S.S.: Designing Masking Fault-Tolerance via Nonmasking Fault-Tolerance. IEEE Trans. Software Eng. 24, 435–450 (1998)
Ghosh, S., Gupta, A., Herman, T., Pemmaraju, S.V.: Fault-Containing Self-Stabilizing Algorithms. In: PODC, pp. 45–54 (1996)
Ghosh, S., Pemmaraju, S.V.: Tradeoffs in fault-containing self-stabilization. In: WSS, pp. 157–169 (1997)
Beauquier, J., Gradinariu, M., Johnen, C.: Randomized Self-Stabilizing and Space Optimal Leader Election under Arbitrary Scheduler on Rings. Distributed Computing 20, 75–93 (2007)
Aljazzar, H., Leue, S.: Debugging of Dependability Models Using Interactive Visualization of Counterexamples. In: QEST, pp. 189–198. IEEE Computer Society, Los Alamitos (2008)
Dolev, S., Israeli, A., Moran, S.: Self-Stabilization of Dynamic Systems Assuming Only Read/Write Atomicity. Distributed Computing 7, 3–16 (1993)
Trivedi, K.S.: Probability and Statistics with Reliability, Queuing, and Computer Science Applications. John Wiley and Sons, Chichester (2001)
Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Wimmer, R., Braitling, B., Becker, B.: Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366–380. Springer, Heidelberg (2009)
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL, pp. 238–252 (1977)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Balaban, I., Pnueli, A., Zuck, L.: Modular Ranking Abstraction. Int. J. Found. Comput. Sci. 18, 5–44 (2007)
Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008)
Kessels, J.L.W.: An Exercise in Proving Self-Stabilization with a Variant Function. Inf. Process. Lett. 29, 39–42 (1988)
Oehlerking, J., Dhama, A., Theel, O.: Towards Automatic Convergence Verification of Self-Stabilizing Algorithms. In: Tixeuil, S., Herman, T. (eds.) SSS 2005. LNCS, vol. 3764, pp. 198–213. Springer, Heidelberg (2005)
Gouda, M.G., Multari, N.J.: Stabilizing Communication Protocols. IEEE Trans. Computers 40, 448–458 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dhama, A., Theel, O., Crouzen, P., Hermanns, H., Wimmer, R., Becker, B. (2009). Dependability Engineering of Silent Self-stabilizing Systems. In: Guerraoui, R., Petit, F. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2009. Lecture Notes in Computer Science, vol 5873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05118-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-05118-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05117-3
Online ISBN: 978-3-642-05118-0
eBook Packages: Computer ScienceComputer Science (R0)