nach oben

International Journal of Parallel Programming

Erschienen in:

01.08.2014

Bringing Coq into the World of GCM Distributed Applications

verfasst von: Nuno Gaspar, Ludovic Henrio, Eric Madelaine

Erschienen in: International Journal of Parallel Programming | Ausgabe 4/2014

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel MulticoreBSP for C: A High-Performance Library for Shared-Memory Parallel Programming

Nächster Artikel Engineering Energy Efficient Visual Sensor Network Applications Using Skeletons

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

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.

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

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/.

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)CrossRef

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)CrossRef

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)CrossRef

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)

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)CrossRef

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)CrossRefMATHMathSciNet

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)

Titel: Bringing Coq into the World of GCM Distributed Applications
verfasst von: Nuno Gaspar
Ludovic Henrio
Eric Madelaine
Publikationsdatum: 01.08.2014
Verlag: Springer US
Erschienen in: International Journal of Parallel Programming / Ausgabe 4/2014
Print ISSN: 0885-7458
Elektronische ISSN: 1573-7640
DOI: https://doi.org/10.1007/s10766-013-0264-7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2014

Engineering Energy Efficient Visual Sensor Network Applications Using Skeletons

Cost-Directed Refactoring for Parallel Erlang Programs

Efficient Abstractions for GPGPU Programming

An Automatic Fusion Mechanism for Variable-Length List Skeletons in SkeTo

MulticoreBSP for C: A High-Performance Library for Shared-Memory Parallel Programming

Dynamic and Speculative Polyhedral Parallelization Using Compiler-Generated Skeletons