A Theory of Fault Recovery for Component-Based Models

  • Borzoo Bonakdarpour
  • Marius Bozga
  • Gregor Gössler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7596)


This paper introduces a theory of fault recovery for component-based models. We specify a model in terms of a set of atomic components incrementally composed and synchronized by a set of glue operators. We define what it means for such models to provide a recovery mechanism, so that the model converges to its normal behavior in the presence of faults (e.g., in self-stabilizing systems). We identify corrector components whose presence in a model is essential to guarantee recovery after the occurrence of faults. We also formalize component-based models that effectively separate recovery from functional concerns. We also show that any model that provides fault recovery can be transformed into an equivalent model, where functional and recovery tasks are modularized in different components.


Fault-tolerance Transformation Separation of concerns BIP 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: ACM International Conference on Embedded Software (EMSOFT), pp. 229–238 (2010)Google Scholar
  2. 2.
    Arora, A., Gouda, M.G.: Closure and convergence: A foundation of fault-tolerant computing. IEEE Transactions on Software Engineering 19(11), 1015–1027 (1993)CrossRefGoogle Scholar
  3. 3.
    Arora, A., Kulkarni, S.S.: Detectors and correctors: A theory of fault-tolerance components. In: International Conference on Distributed Computing Systems (ICDCS), pp. 436–443 (1998)Google Scholar
  4. 4.
    Basu, A., Bonakdarpour, B., Bozga, M., Sifakis, J.: Systematic Correct Construction of Self-stabilizing Systems: A Case Study. In: Dolev, S., Cobb, J., Fischer, M., Yung, M. (eds.) SSS 2010. LNCS, vol. 6366, pp. 4–18. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Springer Journal on Distributed Computing, DC (to appear, 2012)Google Scholar
  6. 6.
    Bonakdarpour, B., Kulkarni, S.S.: Compositional verification of real-time fault-tolerant programs. In: ACM International Conference on Embedded Software (EMSOFT), pp. 29–38 (2009)Google Scholar
  7. 7.
    Bonakdarpour, B., Kulkarni, S.S., Arora, A.: Disassembling real-time fault-tolerant programs. In: ACM International Conference on Embedded Software (EMSOFT), pp. 169–178 (2008)Google Scholar
  8. 8.
    Bozga, M., Sfyrla, V., Sifakis, J.: Modeling synchronous systems in BIP. In: ACM International Conference on Embedded Software (EMSOFT), pp. 77–86 (2009)Google Scholar
  9. 9.
    Brukman, O., Dolev, S.: Recovery oriented programming: runtime monitoring of safety and liveness. Springer Journal on Software Tools for Technology Transfer (STTT) 13(4), 377–395 (2011)Google Scholar
  10. 10.
    Elmqvist, J., Nadjm-Tehrani, S., Minea, M.: Safety Interfaces for Component-Based Systems. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol. 3688, pp. 246–260. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Gärtner, F.C.: Transformational approaches to the specification and verification of fault-tolerant systems: Formal background and classification. Journal of Universal Computer Science 5(10), 668–692 (1999)zbMATHGoogle Scholar
  12. 12.
    Gössler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55(1-3), 161–183 (2005)zbMATHCrossRefGoogle Scholar
  13. 13.
    Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems (TOPLAS) 16, 872–923 (1994)CrossRefGoogle Scholar
  14. 14.
    Leal, W., Arora, A.: Scalable self-stabilization via composition. In: Distributed Computing Systems (ICDCS), pp. 12–21 (2004)Google Scholar
  15. 15.
    Liu, Z., Joseph, M.: Transformation of programs for fault-tolerance. Formal Aspects of Computing 4(5), 442–469 (1992)zbMATHCrossRefGoogle Scholar
  16. 16.
    Liu, Z., Joseph, M.: Specification and verification of fault-tolerance, timing, and scheduling. ACM Transactions on Programming Languages and Systems (TOPLAS) 21(1), 46–89 (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Borzoo Bonakdarpour
    • 1
  • Marius Bozga
    • 2
  • Gregor Gössler
    • 3
  1. 1.School of Computer ScienceUniversity of WaterlooCanada
  2. 2.VERIMAG/CNRSGieresFrance
  3. 3.INRIA-GrenobleMontbonnotFrance

Personalised recommendations