Advertisement

Verifying Safety of Fault-Tolerant Distributed Components

  • Rabéa Ameur-Boulifa
  • Raluca Halalai
  • Ludovic Henrio
  • Eric Madelaine
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7253)

Abstract

We show how to ensure correctness and fault-tolerance of distributed components by behavioural specification. We specify a system combining a simple distributed component application and a fault-tolerance mechanism. We choose to encode the most general and the most demanding kind of faults, byzantine failures, but only for some of the components of our system. With Byzantine failures a faulty process can have any behaviour, thus replication is the only convenient classical solution; this greatly increases the size of the system, and makes model-checking a challenge. Despite the simplicity of our application, full study of the overall behaviour of the combined system requires us putting together the specification for many features required by either the distributed application or the fault-tolerant protocol: our system encodes hierarchical component structure, asynchronous communication with futures, replication, group communication, an agreement protocol, and faulty components. The system we obtain is huge and we have proved its correctness by using at the same time data abstraction, compositional minimization, and distributed model-checking.

Keywords

Asynchronous Communication Read Request Faulty Process Faulty Component Request Queue 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural models for distributed Fractal components. Annals of Télécommunications 64(1-2), 25–43 (2009)CrossRefGoogle Scholar
  2. 2.
    Baude, F., Caromel, D., Dalmasso, C., Danelutto, M., Getov, V., Henrio, L., Pérez, C.: GCM: a grid extension to Fractal for autonomous distributed components. Annals of Télécommunications (2009)Google Scholar
  3. 3.
    Beisiegel, M., Blohm, H., Booz, D., Edwards, M., Hurley, O.: SCA service component architecture, assembly model specification. Technical report (March 2007)Google Scholar
  4. 4.
    Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: Compositional verification for component-based systems and application. IET Software 4(3) (2010)Google Scholar
  5. 5.
    Berthomieu, B., Bodeveix, J.P., Filali, M., Garavel, H., Lang, F., Peres, F., Saad, R., Stoecker, J., Vernadat, F.: The syntax and semantics of Fiacre. In: Rapport LAAS #07264 Rapport de Contrat Projet OpenEmbeDD (Mai 2007)Google Scholar
  6. 6.
    Ameur Boulifa, R., Halalai, R., Henrio, L., Madelaine, E.: Verifying safety of fault-tolerant distributed components (extended version). Research Report RR-7717, INRIA (August 2011)Google Scholar
  7. 7.
    Ameur Boulifa, R., Henrio, L., Madelaine, E.: Behavioural models for group communications. In: WCSI 2010: International Workshop on Component and Service Interoperability, Malaga, Spain (2010)Google Scholar
  8. 8.
    Cansado, A., Madelaine, E.: Specification and Verification for Grid Component-Based Applications: From Models to Tools. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 180–203. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Cleaveland, R., Riely, J.: Testing-Based Abstractions for Value-Passing Systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 417–432. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  10. 10.
    Eker, J., Janneck, J., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Sachs, S., Xiong, Y.: Taming heterogeneity - the ptolemy approach. Proceedings of the IEEE 91(1), 127–144 (2003)CrossRefGoogle Scholar
  11. 11.
    Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  12. 12.
    Garavel, H., Mateescu, R., Bergamini, D., Curic, A., Descoubes, N., Joubert, C., Smarandache-Sturm, I., Stragier, G.: DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 445–449. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Grabe, I., Steffen, M., Torjusen, A.B.: Executable Interface Specifications for Testing Asynchronous Creol Components. Research Report 375. University of Oslo, Dept. of Computer Science (July 2008)Google Scholar
  14. 14.
    Guerraoui, R., Knežević, N., Quéma, V., Vukolić, M.: The next 700 BFT protocols. In: Proceedings of the 5th European Conference on Computer Systems, EuroSys 2010, pp. 363–376. ACM, New York (2010)CrossRefGoogle Scholar
  15. 15.
    Harel, D.: Statecharts: A visual formalism for complex systems (1987)Google Scholar
  16. 16.
    Hatcliff, J., Deng, W., Dwyer, M.B., Jung, G., Ranganath, V.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: Proc. of the 25th Int. Conf. on Software Engineering (2003)Google Scholar
  17. 17.
    Henrio, L., Kammüller, F., Rivera, M.: An Asynchronous Distributed Component Model and its Semantics. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 159–179. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  18. 18.
    Henrio, L., Madelaine, E.: Experiments with distributed model-checking of group-based applications. In: Sophia-Antipolis Formal Analysis Workshop, France Sophia-Antipolis, p. 3 (October 2010)Google Scholar
  19. 19.
    Johnsen, E.B., Owe, O., Yu, I.C.: Creol: a types-safe object-oriented model for distributed concurrent systems. Journal of Theoretical Computer Science 365(1-2), 23–66 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  20. 20.
    Jung, G., Hatcliff, J.: A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures. Science of Computer Programming 75(7), 615–637 (2010)zbMATHCrossRefGoogle Scholar
  21. 21.
    Kotla, R., Alvisi, L., Dahlin, M., Clement, A., Wong, E.: Zyzzyva: speculative byzantine fault tolerance. In: Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP 2007, pp. 45–58. ACM, New York (2007)CrossRefGoogle Scholar
  22. 22.
    Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Trans. Program. Lang. Syst. 4, 382–401 (1982)zbMATHCrossRefGoogle Scholar
  23. 23.
    Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Sere, K., Cuellar, J., Maibaum, T.S.E. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  24. 24.
    Parizek, P., Plasil, F.: Assume-guarantee verification of software components in sofa 2 framework. IET Software 4(3), 210–211 (2010)CrossRefGoogle Scholar
  25. 25.
    Queille, J.-P., Sifakis, J.: Fairness and Related Properties in Transition Systems — A Temporal Logic to Deal with Fairness. Acta Informatica 19, 195–220 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  26. 26.
    Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv. 22, 299–319 (1990)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Rabéa Ameur-Boulifa
    • 1
  • Raluca Halalai
    • 2
  • Ludovic Henrio
    • 3
  • Eric Madelaine
    • 3
  1. 1.Institut TelecomTelecom ParisTech, LTCI CNRSSophia-AntipolisFrance
  2. 2.Technical University of Cluj-NapocaClujRomania
  3. 3.INRIA-I3S-CNRS, University of Nice Sophia AntipolisFrance

Personalised recommendations