. Utils, getPAMulticastController( this.hostComponent).bindGCMMulticast( " M1

P. Hnetrynka, F. Plá?il, V. Mencl, and L. Kapova, SOFA 2.0 metamodel. technical report, 2005.

A. Basu, S. Bensalem, M. Bozga, J. Combaz, M. Jaber et al., Rigorous Component-Based System Design Using the BIP Framework, IEEE Software, vol.28, issue.3, pp.41-48, 2011.
DOI : 10.1109/MS.2011.27

URL : https://hal.archives-ouvertes.fr/hal-00722395

M. Object and . Group, CORBA Component Model 4.0 Specification. Specification Version 4.0. Object Management Group, 0195.

F. Baude, D. Caromel, C. Dalmasso, M. Danelutto, V. Getov et al., GCM: a grid extension to Fractal for autonomous distributed components, annals of telecommunications - annales des t??l??communications, vol.36, issue.1, pp.5-24, 2009.
DOI : 10.1007/s12243-008-0068-8

URL : https://hal.archives-ouvertes.fr/inria-00323919

M. Völter, T. Stahl, J. Bettin, A. Haase, and S. Helsen, Model-driven software development: technology, engineering, management, 2013.

. Obeo, Uml to Java Generator. last visited: 08.2016. url: http : / / marketplace.obeonetwork.com/module, p.2

B. Pagès, BOUML -a UML 2 tool box. last visited: 08

M. Leonor, J. A. Barroca, and . Mcdermid, Formal Methods: Use and Relevance for the Development of Safety Critical Systems, The Computer Journal, vol.35, pp.579-599, 1992.

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker et al., How Amazon web services uses formal methods, Communications of the ACM, vol.58, issue.4, pp.66-73, 2015.
DOI : 10.1145/2699417

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, Model checking programs, Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp.203-232, 2003.
DOI : 10.1109/ASE.2000.873645

T. Bochot, P. Virelizier, H. Waeselynck, and V. Wiels, Model checking flight control systems: The Airbus experience " . In: Software Engineering -Companion Volume, 31st International Conference on, pp.18-27, 2009.

P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem, 1995.

A. Emerson and A. P. Sistla, Symmetry and model checking, In: Formal Methods in System Design, vol.91, pp.105-131, 1996.

L. Henrio, F. Kammüller, and M. Rivera, An Asynchronous Distributed Component Model and Its Semantics, Revised Lectures, Formal Methods for Components and Objects: 7th International Symposium, pp.159-179, 2008.

M. Sirjani, In: Formal Methods for Components and Objects, 5th International Symposium, pp.102-126, 2006.

A. Cansado and E. Madelaine, Formal Methods for Components and Objects: 7th International Symposium Revised Lectures Specification and Verification for Grid Component-Based Applications: From Models to Tools, pp.180-203, 2008.

S. Ahumada, L. Apvrille, T. Barros, A. Cansado, E. Madelaine et al., Specifying Fractal and GCM Components with UML, XXVI International Conference of the Chilean Society of Computer Science (SCCC'07), pp.53-62, 2007.
DOI : 10.1109/SCCC.2007.21

L. Henrio, E. Madelaine, and M. Zhang, pNets: an Expressive Model for Parameterised Networks of Processes In: Formal Approaches to Parallel and Distributed Systems (4PAD)-Special Session of Parallel, Distributed and network-based Processing (PDP), pp.2015-2042

N. Coste, H. Garavel, H. Hermanns, F. Lang, R. Mateescu et al., Ten Years of Performance Evaluation for Concurrent Systems Using CADP, 4th International Symposium on Leveraging Applications of Formal Methods, 2010.
DOI : 10.1007/978-3-642-16561-0_18

URL : https://hal.archives-ouvertes.fr/inria-00532914

N. Gaspar, L. Henrio, and E. Madelaine, Formally Reasoning on a Reconfigurable Component-Based System ??? A Case Study for the Industrial World, Formal Aspects of Component Software -10th International Symposium , FACS 2013, pp.137-156, 2013.
DOI : 10.1007/978-3-319-07602-7_10

URL : https://hal.archives-ouvertes.fr/hal-00916115

R. Ameur-boulifa, R. Halalai, L. Henrio, and E. Madelaine, Verifying Safety of Fault-Tolerant Distributed Components Revised Selected Papers, Formal Aspects of Component Software: 8th International Symposium, pp.278-295, 2011.

E. Bruneton, T. Coupaye, M. Leclercq, V. Quéma, and J. Stefani, The FRACTAL component model and its support in Java, Software: Practice and Experience, vol.6, issue.11-12, pp.11-12, 2006.
DOI : 10.1002/spe.767

F. Baude, L. Henrio, and C. Ruz, Programming distributed and adaptable autonomous components-the GCM/ProActive framework, Software: Practice and Experience, vol.24, issue.13, pp.1189-1227, 2015.
DOI : 10.1002/spe.2270

URL : https://hal.archives-ouvertes.fr/hal-01001043

R. G. Lavender, D. C. Schmidt-john, M. Vlissides, J. O. Coplien, and N. L. Kerth, Pattern Languages of Program Design 2, Active Object: An Object Behavioral Pattern for Concurrent Programming, pp.483-499, 1996.

L. Henrio, F. Huet, and Z. István, Coordination Models and Languages, 15th International Conference Proceedings " . In Multithreaded Active Objects, pp.90-104, 2013.

L. Henrio and J. Rochas, Declarative scheduling for active objects, Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC '14, pp.1-6, 2014.
DOI : 10.1145/2554850.2554957

URL : https://hal.archives-ouvertes.fr/hal-00916293

T. Barros, R. Ameur-boulifa, A. Cansado, L. Henrio, and E. Madelaine, Behavioural models for distributed Fractal components, annals of telecommunications - annales des t??l??communications, vol.5, issue.1, pp.25-43, 2009.
DOI : 10.1007/s12243-008-0069-7

URL : https://hal.archives-ouvertes.fr/inria-00268965

L. Henrio, E. Madelaine, and M. Zhang, A Theory for the Composition of Concurrent Processes, Formal Techniques for Distributed Objects , Components, and Systems -36th IFIP WG 6.1 International Conference Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, pp.175-194, 0198.
DOI : 10.1007/978-3-319-39570-8_12

URL : https://hal.archives-ouvertes.fr/hal-01432917

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP 2011: a toolbox for the construction and analysis of distributed processes, International Journal on Software Tools for Technology Transfer, vol.1, issue.1/2, pp.89-107, 2013.
DOI : 10.1007/s10009-012-0244-z

URL : https://hal.archives-ouvertes.fr/hal-00715056

R. Abid, G. Salaün, F. Bongiovanni, and N. Palma, Verification of a Dynamic Management Protocol for Cloud Applications, 11th International Symposium, ATVA 2013, pp.178-192, 2013.
DOI : 10.1007/978-3-319-02444-8_14

URL : https://hal.archives-ouvertes.fr/hal-00863262

G. Chalupar, S. Peherstorfer, E. Poll, and J. De-ruiter, Automated Reverse Engineering using Lego R ?, 8th USENIX Workshop on Offensive Technologies, 2014.

B. Theelen, J. Katoen, and H. Wu, Model checking of Scenario-Aware Dataflow with CADP, 2012 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp.2012-653
DOI : 10.1109/DATE.2012.6176552

T. Bolognesi and E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, vol.14, issue.1, pp.25-59, 1987.
DOI : 10.1016/0169-7552(87)90085-7

F. Lang, Jean-François Pradat-Peyre, and Véronique Viguié Donzeau-Gouge, 26th IFIP WG 6.1 International Conference Proceedings " . In: ed. by Elie Najm Chap. Refined Interfaces for Compositional Verification, pp.159-174, 2006.

R. De, N. , and F. Vaandrager, Semantics of Systems of Concurrent Processes: LITP Spring School on Theoretical Computer Science, Proceedings " . In: ed. by Irène Guessarian, 1990.

H. Berlin, Chap. Action versus state based logics for transition systems, pp.407-419, 1990.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263, 1986.
DOI : 10.1145/5397.5399

J. Michael, R. E. Fischer, and . Ladner, Propositional dynamic logic of regular programs, In: Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.

R. Mateescu and M. Sighireanu, Efficient on-the-fly model-checking for regular alternation-free mu-calculus Special issue on Formal Methods for Industrial Critical Systems, In: Science of Computer Programming, vol.463, pp.255-281, 2003.

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, Patterns in Property Specifications for Finite-state Verification, Proceedings of the 21st International Conference on Software Engineering. ICSE '99, pp.411-420, 1999.

R. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, pp.148-164, 2008.
DOI : 10.1007/978-3-540-68237-0_12

URL : https://hal.archives-ouvertes.fr/inria-00315312

H. Andersen, Model checking and boolean graphs, In: Theoretical Computer Science, vol.1261, pp.3-30, 1994.

H. Garavel and F. Lang, Formal Techniques for Networked and Distributed Systems: FORTE, IFIP TC6/WG6.1 ? 21st International Conference on Formal Techniques for Networked and Distributed Systems SVL: A Scripting Language for Compositional Verification, pp.377-392, 2001.

H. Garavel, R. Mateescu, and W. Serwe, Large-scale Distributed Verification Using CADP: Beyond Clusters to Grids, Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling (PASM) and the Eleventh International Workshop on Parallel and Distributed Methods in Verification (PDMC), pp.145-161, 2013.
DOI : 10.1016/j.entcs.2013.07.010

URL : https://hal.archives-ouvertes.fr/hal-00730668

B. Berthomieu, J. P. Bodeveix, M. Filali, H. Garavel, F. Lang et al., The syntax and semantics of Fiacre, 2009.

A. Rodrigues and D. Silva, Model-driven engineering: A survey supported by the unified conceptual model, Computer Languages, Systems & Structures, vol.43, pp.139-155, 2015.
DOI : 10.1016/j.cl.2015.06.001

D. Steinberg, F. Budinsky, M. Paternostro, and E. Merks, EMF: Eclipse Modeling Framework, 2008.

. Graphical-modeling and . Framework, url: http : / / www . eclipse . org / gmf tooling, p.36

U. Eclipse, url: https : / / wiki . eclipse . org, pp.36-52

E. Juliot and J. Benois, Viewpoints creation using Obeo Designer or how to build Eclipse DSM without being an expert developer. Obeo (cit, p.36

. Acceleo-code-generator, url: http://wiki.eclipse.org/Acceleo (cit, p.37

A. Cansado, D. Caromel, L. Henrio, E. Madelaine, M. Rivera et al., A Specification Language for Distributed Components Implemented in GCM/ProActive, pp.418-448, 2008.
DOI : 10.1007/978-3-540-85289-6_16

A. Ressouche, R. De-simone, V. Bouali, and . Roy, The FC2Tool user manuel url: http://www-sop.inria.fr/meije, p.38, 1994.

T. Barros, Formal specification and verification of distributed component systems, 2005.
URL : https://hal.archives-ouvertes.fr/tel-00090718

A. Cansado, L. Henrio, and E. Madelaine, Transparent First-class Futures and Distributed Components, Proceedings of the 5th International Workshop on Formal Aspects of Component Software, pp.155-171, 2008.
DOI : 10.1016/j.entcs.2009.12.036

URL : https://hal.archives-ouvertes.fr/inria-00311515

L. Rabéa-ameur-boulifa, E. Henrio, and . Madelaine, Behavioural Models for Group Communications, WCSI-10: International Workshop on Component and Service Interoperability, 2010.

L. Henrio, O. Kulankhina, S. Li, and E. Madelaine, Integrated environment for verifying and running distributed components - Extended version, p.24, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01252323

L. Gary and . Peterson, An O(Nlog N) Unidirectional Algorithm for the Circular Extrema Problem, In: ACM Trans. Program. Lang. Syst, vol.4, issue.4, pp.758-762, 1982.

D. Dolev, M. M. Klawe, and M. Rodeh, An O(n log n) unidirectional distributed algorithm for extrema finding in a circle, Journal of Algorithms, vol.3, issue.3, pp.245-260, 1982.
DOI : 10.1016/0196-6774(82)90023-2

P. Naoumenko, Designing Non-functional Aspects With Components, pp.56-70

C. Canal, C. S. Pasareanu, A. Cansado, L. Henrio, E. Madelaine et al., Proceedings of the 5th International Workshop on Formal Aspects of Component Software (FACS 2008) Unifying Architectural and Behavioural Specifications of Distributed Components, In: Electronic Notes in Theoretical Computer Science, vol.260, pp.25-45, 2010.

N. Gaspar, L. Henrio, and E. Madelaine, Painless Support for Static and Runtime Verification of Component-Based Applications, p.15, 2015.
DOI : 10.1007/978-3-319-24644-4_18

URL : https://hal.archives-ouvertes.fr/hal-01446604

. Papyrus and . Environment, url: https://eclipse

R. Ameur-boulifa, L. Henrio, E. Madelaine, and A. Savu, Behavioural semantics for asynchronous components, Journal of Logical and Algebraic Methods in Programming, vol.89, issue.209, pp.58-60, 2012.
DOI : 10.1016/j.jlamp.2017.02.003

URL : https://hal.archives-ouvertes.fr/hal-00761073

N. Gaspar, L. Henrio, and E. Madelaine, Bringing Coq into the World of GCM Distributed Applications, International Symposium on High-level Parallel Programming and Applications&, HLPP, pp.2013-76
DOI : 10.1007/s10766-013-0264-7

URL : https://hal.archives-ouvertes.fr/hal-00880533

L. Henrio, O. Kulankhina, D. Liu, and E. Madelaine, Verifying the correct composition of distributed components: Formalisation and Tool, Proceedings 13th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems, FOCLASA 2014, pp.69-85, 2014.
DOI : 10.4204/EPTCS.175.5

URL : https://hal.archives-ouvertes.fr/hal-01055370

J. Warmer and A. Kleppe, The Object Constraint Language: Getting Your Models Ready for MDA, 2003.

M. Malohlava, P. Hnetynka, and T. Bure?, SOFA 2 Component Framework and Its Ecosystem, Proceedings the 9th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA), pp.101-106, 2013.
DOI : 10.1016/j.entcs.2013.04.009

L. Seinturier, N. Pessemier, L. Duchien, and T. Coupaye, A Component Model Engineered with Components and Aspects, Proceedings of the 9th International SIGSOFT Symposium on Component-Based Software Engineering, 2006.
DOI : 10.1007/11783565_10

URL : https://hal.archives-ouvertes.fr/inria-00126350

P. Merle and J. Stefani, A formal specification of the Fractal component model in Alloy, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00338987

L. Henrio, F. Kammüller, and M. Khan, A Framework for Reasoning on Component Composition, Lecture Notes in Computer Science, vol.96, issue.1, 2009.
DOI : 10.1007/3-540-45949-9

URL : https://hal.archives-ouvertes.fr/inria-00490380

Y. Bertot, Coq in a Hurry, p.603118, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00001173

J. Architecture and . Binding, url: https://jaxb.java.net

H. J. Köhler, U. Nickel, J. Niere, and A. Zündorf, Integrating UML Diagrams for Production Control Systems, Proceedings of the 22Nd International Conference on Software Engineering. ICSE '00, pp.241-251, 2000.

I. Azim, N. , and J. Tanaka, Code Generation From Uml Statecharts, Proc. 7 th IASTED International Conf. on Software Engineering and Application (SEA 2003), pp.315-321, 2003.

E. Sekerinski and R. Zurob, iState: A Statechart Translator, UML 2001 ? The Unified Modeling Language. Modeling Languages, Concepts, and Tools: 4th International Conference, pp.376-390, 2001.
DOI : 10.1007/3-540-45441-1_28

A. Viewer-for-proactive-active and . Objects, url: https://github.com/scaleproactive/A-viewer-tool-for-multiactive-objects .git (cit, p.123

A. Rouini, Parametric Component Topologies: language extension and implementation, 2010.

K. Rustan, M. Leino, and M. Moskal, VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0, Proceedings of Tools and Experiments Workshop at VSTTE. 2010 (cit, p.162

T. Aubonnet, L. Henrio, S. Kessal, O. Kulankhina, F. Lemoine et al., Management of service composition based on self-controlled components, Journal of Internet Services and Applications, vol.615, p.17, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01180627

M. Ibañez, C. Ruz, L. Henrio, and J. Bustos-jiménez, Reconfigurable Applications Using GCMScript " . Accepted at IEEE Cloud computing . Special issue: Autonomic clouds, 2016.

P. Hn?tynka and F. Plá?il, Dynamic Reconfiguration and Access to Services in Hierarchical Component Models, Proceedings of the 9th International Conference on Component-Based Software Engineering. CBSE'06
DOI : 10.1007/11783565_27

T. Bure? and F. Plá?il, Communication Style Driven Connector Configurations, p.3026

T. Bure? and F. Plá?il, Generating Connectors for Homogeneous and Heterogeneous Deployment, p.2006

F. Plá?il and S. Visnovsky, Behavior protocols for software components, IEEE Transactions on Software Engineering, vol.28, issue.11, pp.1056-1076, 2002.
DOI : 10.1109/TSE.2002.1049404

M. Mach, F. Plá?il, and J. Kofron, Behavior Protocol Verification: Fighting State Explosion, International Journal of Computer and Information Science, vol.61, pp.22-30, 2005.

P. Parizek, F. Plá?il, and J. Kofron, Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker, 2006 30th Annual IEEE/NASA Software Engineering Workshop, pp.25-28, 2006.
DOI : 10.1109/SEW.2006.23

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, Model checking programs, Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp.203-232, 2003.
DOI : 10.1109/ASE.2000.873645

J. Gerard and . Holzmann, The Model Checker SPIN, IEEE Trans. Softw. Eng, vol.23, issue.180, pp.279-295, 0197.

J. Kofron, Checking software component behavior using behavior protocols and spin, Proceedings of the 2007 ACM symposium on Applied computing , SAC '07, pp.1513-1517, 2007.
DOI : 10.1145/1244002.1244326

A. Basu, M. Bozga, and J. Sifakis, Modeling Heterogeneous Real-time Components in BIP, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), pp.3-12, 2006.
DOI : 10.1109/SEFM.2006.27

URL : https://hal.archives-ouvertes.fr/hal-00375298

V. Sfyrla, G. Tsiligiannis, I. Safaka, M. Bozga, and J. Sifakis, Compositional translation of simulink models into synchronous BIP, International Symposium on Industrial Embedded System (SIES), pp.217-220, 2010.
DOI : 10.1109/SIES.2010.5551374

URL : https://hal.archives-ouvertes.fr/hal-00558040

A. Mohamed-yassin-chkouri, M. Robert, J. Bozga, and . Sifakis, Translating AADL into BIP - Application to the Verification of Real-Time Systems, Reports and Revised Selected Papers. Lecture Notes in Computer Science, vol.55, pp.5-19, 2008.
DOI : 10.1007/978-3-540-77419-8_5

S. Bensalem, M. Bozga, T. Nguyen, and J. Sifakis, D-Finder: A Tool for Compositional Deadlock Detection and Verification, Computer Aided Verification, 21st International Conference, pp.614-619, 2009.
DOI : 10.1007/978-3-642-02658-4_45

URL : https://hal.archives-ouvertes.fr/hal-00722550

S. Bliudze, A. Cimatti, M. Jaber, S. Mover, M. Roveri et al., Formal Verification of Infinite-State BIP Models Automated Technology for Verification and Analysis: 13th International Symposium, Proceedings. Ed. by Bernd Finkbeiner, Geguang Pu, and Lijun Zhang, pp.326-343, 2015.

R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti et al., The nuXmv Symbolic Model Checker, Proceedings of the 16th International Conference on Computer Aided Verification, pp.334-342
DOI : 10.1007/978-3-319-08867-9_22

Y. Falcone, M. Jaber, T. Nguyen, M. Bozga, and S. Bensalem, Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation, Software and System Modeling, pp.173-199, 2015.
DOI : 10.1007/s10270-013-0323-y

URL : https://hal.archives-ouvertes.fr/hal-00972566

B. Bonakdarpour, M. Bozga, and J. Quilbeuf, Automated distributed implementation of component-based models with priorities, Proceedings of the ninth ACM international conference on Embedded software, EMSOFT '11, pp.59-68, 2011.
DOI : 10.1145/2038642.2038654

URL : https://hal.archives-ouvertes.fr/hal-00722405

M. Sirjani, A. Movaghar, A. Shali, and F. S. De-boer, Modeling and Verification of Reactive Systems using Rebeca, In: Fundam. Inform, vol.634, pp.385-410, 2004.

M. Sirjani, F. S. De-boer, and A. Movaghar-rahimabadi, Modular Verification of a Component-Based Actor Language, J. UCS, vol.1110, issue.185, pp.1695-1717, 2005.

F. Alavizadeh and M. Sirjani, Using UML to Develop Verifiable Reactive Systems, Proceedings of the International Conference on Software Engineering Research and Practice & Conference on Programming Languages and Compilers, pp.554-561, 2006.

E. Khamespanah, M. Sirjani, Z. Sabahi-kaviani, R. Khosravi, and M. Izadi, Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system, Science of Computer Programming, vol.98, issue.2, pp.184-204, 2015.
DOI : 10.1016/j.scico.2014.07.005

E. Khamespanah, M. Sirjani, M. R. Mousavi, Z. Sabahi-kaviani, and M. Razzazi, State Distribution Policy for Distributed Model Checking of Actor Models, pp.72-2015

M. Sirjani, A. Movaghar, A. Shali, and F. S. De-boer, Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models, J. UCS, vol.116, pp.1054-1082, 2005.

M. Mahdi-jaghoori, M. Sirjani, M. R. Mousavi, E. Khamespanah, and A. Movaghar, Symmetry and partial order reduction techniques in model checking Rebeca, Acta Informatica, vol.9, issue.2, pp.33-66, 2010.
DOI : 10.1007/s00236-009-0111-x

R. Einar-broch-johnsen, R. Hähnle-schäfer, M. Schlatte, and . Steffen, ABS: A Core Language for Abstract Behavioral Specification " . In: Formal Methods for Components and Objects (FMCO)

C. Chang-din, R. Bubel, and R. Hähnle, KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS, Lecture Notes in Computer Science, vol.9195, issue.188, pp.517-526, 0190.

L. Henrio and J. Rochas, From Modelling to Systematic Deployment of Distributed Active Objects, 11th International Federated Conference on Distributed Computing Techniques, 0191.
DOI : 10.1007/978-3-319-39519-7_13

URL : https://hal.archives-ouvertes.fr/hal-01305474

R. Hähnle, M. Helvenstijn, E. Broch-johnsen, M. Lienhardt, D. Sangiorgi et al., HATS Abstract Behavioral Specification: The Architectural View " . In: FMCO -Formal Methods for Components and Objects -2011, pp.165-185, 2011.

R. Hähnle, The Abstract Behavioral Specification Language: A Tutorial Introduction, Lecture Notes in Computer Science, vol.7866, pp.1-37, 2012.
DOI : 10.1007/978-3-642-40615-7_1

I. C. Jia-chun-lin, E. Yu, M. Broch-johnsen, and . Lee, ABS-YARN: A Formal Framework for Modeling Hadoop YARN Clusters

B. Beckert, R. Hähnle, and P. H. Schmitt, Verification of Objectoriented Software: The KeY Approach, 2007.

E. Giachino, C. Laneve, and M. Lienhardt, A framework for deadlock detection in core??ABS, Software & Systems Modeling, vol.14, issue.5, 2015.
DOI : 10.1007/s10270-014-0444-y

URL : https://hal.archives-ouvertes.fr/hal-01229046

E. Albert, P. Arenas, S. Genaim, M. Gómez-zamalloa, and G. Puebla, COSTABS, Proceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation, PEPM '12, pp.151-154, 2012.
DOI : 10.1145/2103746.2103774

N. Bezirgiannis and F. Boer, SOFSEM 2016: Theory and Practice of Computer Science, 42nd International Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic Proceedings " . In: ed. by R¯ usi¸n?usi¸n? Freivalds M¯ arti¸n?arti¸n? ABS: A High-Level Modeling Language for Cloud-Aware Programming, pp.433-444, 2016.

S. Becker, H. Koziolek, and R. Reussner, Model-Based performance prediction with the palladio component model, Proceedings of the 6th international workshop on Software and performance , WOSP '07, pp.54-65, 2007.
DOI : 10.1145/1216993.1217006

T. Bures, I. Gerostathopoulos, P. Hnetynka, J. Keznikl, M. Kit et al., DEECO, Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering, CBSE '13, pp.81-90, 2013.
DOI : 10.1145/2465449.2465462

T. Bure?, R. Ali, I. Gerostathopoulos, P. Hn?tynka, J. Keznikl et al., DEECo Computational Model -I, 2013.

R. Hennicker and A. Klarl, Foundations for Ensemble Modeling ??? The Helena Approach, Specification, Algebra, and Software: A Festschrift Symposium in Honor of Kokichi Futatsugi, p.2014, 2014.
DOI : 10.1023/A:1010071910869

A. Klarl, L. Cichella, and R. Hennicker, From Helena Ensemble Specifications to Executable Code, Formal Aspects of Component Software -11th International Symposium, FACS 2014, pp.183-190, 2014.
DOI : 10.1007/978-3-319-15317-9_11

A. Klarl and R. Hennicker, Design and Implementation of Dynamically Evolving Ensembles with the Helena Framework, 2014 23rd Australian Software Engineering Conference, pp.15-24, 2014.
DOI : 10.1109/ASWEC.2014.26

A. Klarl, From Helena Ensemble Specifications to Promela Verification Models, Model Checking Software -22nd International Symposium, pp.39-45, 2015.
DOI : 10.1007/978-3-319-23404-5_4

R. Hennicker, A. Klarl, and M. Wirsing, Model-Checking Helena Ensembles with??Spin, pp.331-360, 2015.
DOI : 10.1007/978-3-319-23165-5_16

I. Grabe, M. M. Jaghoori, J. Klein, S. Klüppelholz, A. Stam et al., The Credo Methodology -(Extended Version) Revised Selected Papers, Formal Methods for Components and Objects -8th International Symposium, pp.41-69, 2009.

F. Arbab, Reo: a channel-based coordination model for component composition, Mathematical Structures in Computer Science, vol.14, issue.3, pp.329-366, 2004.
DOI : 10.1017/S0960129504004153

C. Baier, M. Sirjani, F. Arbab, and J. Rutten, Modeling component connectors in Reo by constraint automata, Second International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA'03), pp.75-113, 2006.
DOI : 10.1016/j.scico.2005.10.008

E. Broch, J. , and O. Owe, An Asynchronous Communication Model for Distributed Concurrent Objects, In: Software and Systems Modeling, vol.6, issue.1, pp.35-58, 2007.

I. Grabe, M. Kyas, M. Steffen, and A. B. Torjusen, Revised Selected Papers, Fundamentals of Software Engineering: Third IPM International Conference Executable Interface Specifications for Testing Asynchronous Creol Components, pp.324-339, 2009.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Mart?-oliet et al., Maude: specification and programming in rewriting logic Rewriting Logic and its Applications, In: Theoretical Computer Science, vol.2852, pp.187-243, 0199.

J. Hatcliff, X. Deng, M. B. Dwyer, G. Jung, and V. Prasad-ranganath, Cadena: an integrated development, analysis, and verification environment for component-based systems, 25th International Conference on Software Engineering, 2003. Proceedings., pp.160-173, 2003.
DOI : 10.1109/ICSE.2003.1201197

M. B. Robby, J. Dwyer, and . Hatcliff, Bogor: An Extensible and Highly-modular Software Model Checking Framework

C. Demartini, R. Iosif, and R. Sisto, dSPIN: A Dynamic Extension of SPIN, Proceedings. Lecture Notes in Computer Science, vol.1680, pp.261-276, 1999.
DOI : 10.1007/3-540-48234-2_20

M. Bozga, S. Graf, and L. Mounier, Automated validation of distributed software using the IF environment, Electronic Notes in Theoretical Computer Science, vol.55, issue.3, pp.370-381, 2001.
DOI : 10.1016/S1571-0661(04)00263-4

URL : https://hal.archives-ouvertes.fr/hal-00374652

S. Yovine, KRONOS: a??verification tool for real-time systems, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.123-133, 1997.
DOI : 10.1007/s100090050009

G. De, R. , and A. Santone, An Eclipse-based Editor to Support LOTOS Newcomers, Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), 2014 IEEE 23rd International Conference on. 2014, pp.372-377

H. Evrard and F. Lang, Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes, 2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, 2015.
DOI : 10.1109/PDP.2015.96

URL : https://hal.archives-ouvertes.fr/hal-01086522

J. Gerard and . Holzmann, Design and Validation of Computer Protocols, 1991.

G. J. Holzmann and M. H. Smith, An automated verification method for distributed systems software based on model extraction, IEEE Transactions on Software Engineering, vol.28, issue.4, pp.364-377, 2002.
DOI : 10.1109/TSE.2002.995426

J. Gerard, D. Holzmann, and . Bosnacki, The Design of a Multicore Extension of the SPIN Model Checker, IEEE Trans. Softw. Eng, vol.3310, pp.659-674, 2007.

D. Peled, Combining Partial Order Reductions with On-the-fly Model- Checking, Proceedings of the 6th International Conference on Computer Aided Verification. CAV '94, pp.377-390, 1994.

M. Kamel and S. Leue, Validation of a Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin, In: International SPIN Workshop

M. Lowry, K. Havelund, and J. Penix, Formal Analysis of a Space Craft Controller using Spin, In: International SPIN Workshop

G. Lüttgen and V. Carreño, Analyzing Mode Confusion via Model Checking, In: International SPIN Workshop
DOI : 10.1007/3-540-48234-2_9

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking, Proc. International Conference on Computer- Aided Verification, 2002.

K. L. Mcmillan, Symbolic Model Checking, 1993.

A. Cimatti, E. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani et al., Integrating BDD-Based and SAT-Based Symbolic Model Checking, Proc. " Frontiers of Combining Systems, FROCOS'02, 2002.
DOI : 10.1007/3-540-45988-X_5

S. Berezin, S. Campos, and E. M. Clarke, Compositional Reasoning in Model Checking, 1998.
DOI : 10.1007/3-540-49213-5_4

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001.
DOI : 10.1145/378239.379017

B. Kolb, M. Völter, D. Ratiu, and D. Pavletic, Kolja Dummann , and Tamás Szabó

J. Vander-meulen and C. Pecheur, Efficient Symbolic Model Checking for Process Algebras, LNCS, vol.46, issue.3, 2008.
DOI : 10.1007/3-540-48257-1_14

S. Escobar and J. Meseguer, Symbolic Model Checking of Infinitestate Systems Using Narrowing, Proceedings of the 18th International Conference on Term Rewriting and Applications. RTA'07, pp.153-168, 2007.

A. Farzan and J. Meseguer, Partial Order Reduction for Rewriting Semantics of Programming Languages, Proceedings of the 6th International Workshop on Rewriting Logic and its Applications (WRLA). Ed. by G. Denker and C. Talcott, 2006.
DOI : 10.1016/j.entcs.2007.06.008

L. Henrio and J. Rochas, Declarative scheduling for active objects, Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC '14, pp.1339-1344, 2014.
DOI : 10.1145/2554850.2554957

URL : https://hal.archives-ouvertes.fr/hal-00916293

L. Henrio and M. Rivera, Stopping safely hierarchical distributed components, Proceedings of the 2008 compFrame/HPC-GECO workshop on Component based high performance, CBHPC '08
DOI : 10.1145/1456190.1456201