Skip to main content
Log in

Bringing Coq into the World of GCM Distributed Applications

  • Published:
International Journal of Parallel Programming Aims and scope Submit manuscript

Abstract

Among all programming paradigms, component-based engineering stands as one of the most followed approaches for real world software development. Its emphasis on clean separation of concerns and reusability makes it appealing for both industrial and research purposes. The Grid Component Model (GCM) endorses this approach in the context of distributed systems by providing all the means to define, compose and dynamically reconfigure component-based applications. While structural reconfiguration is one of the key features of GCM applications, this ability to evolve at runtime poses several challenges w.r.t reliability. In this paper we present Mefresa, a framework for reasoning on the structure of GCM applications. This contribution comes in the form of a formal specification mechanized in the Coq Proof Assistant. Our aim is to demonstrate the benefits of interactive theorem proving for the reasoning on software architectures. We provide a configuration and reconfiguration language for the safe instantiation of distributed systems.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. More information concerning GCM/ProActive can be found at http://proactive.inria.fr/.

  2. Mefresa is continuously being updated at: http://www-sop.inria.fr/members/Nuno.Gaspar/Mefresa.php.

  3. The element \(\rightarrow \) field notation is used for projections.

  4. In Figs. 2, 3 and 4 we use uppercase letters for denoting components, and lowercase ones for interfaces.

  5. We use the common \(id [index]\) notation for indexing id at index index.

  6. GCM components possess a membrane part that we do not model in Mefresa. This however, should not be seen as too much of a shortcoming.

  7. The Spinnaker Project. http://www.spinnaker-rfid.com/.

References

  1. Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural models for distributed fractal components. Ann. Télécommun. 64(1–2), 25–43 (2009)

    Article  Google Scholar 

  2. Barros, T., Cansado, A., Madelaine, E., Rivera, M.: Model-checking distributed components: the vercors platform. Electron. Notes Theor. Comput. Sci. 182, 3–16 (2007). doi:10.1016/j.entcs.2006.09.028

  3. Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the bip framework. IEEE Softw. 28(3), 41–48 (2011)

    Article  Google Scholar 

  4. 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. Ann. Télécommun. 64(1–2), 5–24 (2009)

    Article  Google Scholar 

  5. Baude, F., Henrio, L., Naoumenko, P.: Structural reconfiguration: an autonomic strategy for gcm components. In: Proceedings of The Fifth International Conference on Autonomic and Autonomous Systems: ICAS 2009 (2009)

  6. Bertot, Y.: Coq in a hurry. CoRR abs/cs/0603118 (2006)

  7. Boulifa, R.A., Halalai, R., Henrio, L., Madelaine, E.: Verifying safety of fault-tolerant distributed components. In: International Symposium on Formal Aspects of Component Software (FACS 2011), Lecture Notes in Computer Science. Springer, Oslo (2011)

  8. Bruneton, E., Coupaye, T., Stefani, J.B.: The fractal component model (2004). http://fractal.ow2.org/

  9. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The maude 2.0 system. In: Nieuwenhuis, R. (ed.) Rewriting Techniques and Applications (RTA 2003), no. 2706 in Lecture Notes in Computer Science, pp. 76–87. Springer (2003)

  10. David, P.C., Ledoux, T., Léger, M., Coupaye, T.: Fpath and fscript: language support for navigation and reliable reconfiguration of fractal architectures. Ann. Télécommun. 64(1–2), 45–63 (2009)

    Article  Google Scholar 

  11. Gaspar, N., Madelaine, E.: Fractal à la Coq. In: Conférence en IngénieriE du Logiciel. Rennes, France (2012). http://hal.inria.fr/hal-00725291

  12. Henrio, L., Kammüller, F., Khan, M.U.: A framework for reasoning on component composition. In: FMCO 2009, Lecture Notes in Computer Science. Springer (2010)

  13. Henrio, L., Rivera, M.: Stopping safely hierarchical distributed components: application to gcm. In: CBHPC ’08: Proceedings of the 2008 compFrame/HPC-GECO Workshop on Component Based High Performance, pp. 1–11. ACM, New York, NY, USA (2008). doi:10.1145/1456190.1456201

  14. Hnetynka, P., Plasil, F.: Dynamic reconfiguration and access to services in hierarchical component models. In: Proceedings of CBSE 2006, Vasteras, Sweden, LNCS 4063, pp. 352–359. Springer (2006)

  15. Inverardi, P., Muccini, H., Pelliccione, P.: Charmy: an extensible tool for architectural analysis. In: ESEC-FSE’05, The Fifth Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering. Research Tool, Demos (2005)

  16. Johnsen, E.B., Owe, O., Yu, I.C.: Creol: a type-safe object-oriented model for distributed concurrent systems. Theor. Comput. Sci. 365(1–2), 23–66 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  17. Merle, P., Stefani, J.B.: A formal specification of the fractal component model in alloy. Rapport de recherche RR-6721, INRIA (2008). http://hal.inria.fr/inria-00338987

  18. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a proof assistant for higher-order logic. In: LNCS, vol. 2283. Springer (2002)

  19. Sprenger, C.: A verified model checker for the modal mu-calculus in coq. In: In TACAS, LNCS, vol. 1384. Springer (1998)

  20. The Coq Development Team: The Coq proof assistant reference manual (2012)

Download references

Acknowledgments

Our ingénieur expert Bastien Sauvan deserves a mention for his help and comments concerning the GCM specification. This work is partially supported by the ANR SocEDA and Spinnaker projects.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Nuno Gaspar.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Gaspar, N., Henrio, L. & Madelaine, E. Bringing Coq into the World of GCM Distributed Applications. Int J Parallel Prog 42, 643–662 (2014). https://doi.org/10.1007/s10766-013-0264-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10766-013-0264-7

Keywords

Navigation