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.
Similar content being viewed by others
Notes
More information concerning GCM/ProActive can be found at http://proactive.inria.fr/.
Mefresa is continuously being updated at: http://www-sop.inria.fr/members/Nuno.Gaspar/Mefresa.php.
The element \(\rightarrow \) field notation is used for projections.
We use the common \(id [index]\) notation for indexing id at index index.
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.
The Spinnaker Project. http://www.spinnaker-rfid.com/.
References
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)
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
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)
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)
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)
Bertot, Y.: Coq in a hurry. CoRR abs/cs/0603118 (2006)
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)
Bruneton, E., Coupaye, T., Stefani, J.B.: The fractal component model (2004). http://fractal.ow2.org/
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)
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)
Gaspar, N., Madelaine, E.: Fractal à la Coq. In: Conférence en IngénieriE du Logiciel. Rennes, France (2012). http://hal.inria.fr/hal-00725291
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)
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
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)
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)
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)
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
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a proof assistant for higher-order logic. In: LNCS, vol. 2283. Springer (2002)
Sprenger, C.: A verified model checker for the modal mu-calculus in coq. In: In TACAS, LNCS, vol. 1384. Springer (1998)
The Coq Development Team: The Coq proof assistant reference manual (2012)
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
Corresponding author
Rights 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
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10766-013-0264-7