, Alloy Analyzer Web Site. Accessible

A. Amazon,

. Ansible,

. Aws-cloudformation,

P. Chef,

. Cloudstack,

, Docker Compose Source Code

, HOT Template Structure Specification

, HOT Types Specification

. Iso/iec, Cloud Infrastructure Management Interface (CIMI) Model and RESTful HTTP-based Protocol, 2015.

. Juju,

M. Azure,

. Openstack,

O. Heat,

. Python-ipaddress-library,

, vvp Validation Tool

, OASIS Standard -Topology and Orchestration Specification for Cloud Applications -Version 1.0. Accessible at, 2013.

, Oasis open -tosca test assertions -normative types, 2015.

M. Ahmed-nacer, S. Tata, W. Gaaloul, P. Merle, J. Parpaillon et al., OCCI Behavioural Model, 2016.

L. Bass, P. Clements, and R. Kazman, Software Architecture in Practice, 2013.

J. Bellendorf and Z. A. Mann, Cloud topology and orchestration using TOSCA: A systematic literature review, Service-Oriented and Cloud Computing -7th IFIP WG 2.14 European Conference, vol.11116, 2018.

S. Bliudze and J. Sifakis, A notion of glue expressiveness for component-based systems, CON-CUR, vol.5201, 2008.

A. Brogi, J. Soldani, and P. Wang, TOSCA in a nutshell: Promises and perspectives, 3rd European Conference on Service-Oriented and Cloud Computing, vol.8745, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01318292

E. Bruneton, T. Coupaye, M. Leclercq, V. Quema, and J. B. Stefani, The Fractal Component Model and its Support in Java. Software -Practice and Experience, vol.36, pp.11-12, 2006.

M. Bugliesi, G. Castagna, and S. Crafa, Access control for mobile agents: the calculus of boxed ambients, ACM. Trans. Prog. Languages and Systems, vol.26, issue.1, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00152525

L. Cardelli and A. Gordon, Mobile Ambients. Theoretical Computer Science, vol.240, issue.1, 2000.

R. D. Cosmo, A. Eiche, J. Mauro, S. Zacchiroli, G. Zavattaro et al., Automatic deployment of services in the cloud with aeolus blender, 13th International Conference Service-Oriented Computing (ICSOC), vol.9435, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01233489

R. D. Cosmo, J. Mauro, S. Zacchiroli, and G. Zavattaro, Aeolus: A component model for the cloud, Information and Computation, vol.239, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091062

I. Crnkovic, S. Sentilles, A. Vulgarakis, and M. R. Chaudron, A classification framework for software component models, IEEE Trans. Software Eng, vol.37, issue.5, 2011.

J. Fischer, R. Majumdar, and S. Esmaeilsabzali, Engage: a deployment management system, ACM SIGPLAN Notices, vol.47, pp.263-274, 2012.

D. Garlan, R. T. Monroe, and D. Wile, Acme: Architectural Description of Component-Based Systems, Foundations of Component-Based Systems, 2000.

G. Goessler and J. Sifakis, Composition for component-based modeling, Sci. Comput. Program, vol.55, pp.1-3, 2005.

P. Goldsack, J. Guijarro, S. Loughran, A. Coles, A. A. Farrell et al., The smartfrog configuration management framework, SIGOPS Oper. Syst. Rev, vol.43, issue.1, 2009.

M. Hennessy, J. Rathke, and N. Yoshida, Safedpi: a language for controlling mobile code, Acta Inf, vol.42, pp.4-5, 2005.

J. A. Hewson and P. Anderson, Modelling system administration problems with csps, Constraint Modelling and Reformulation (ModRef'11), 2011.

D. Jackson, Software Abstractions: Logic, Language, and Analysis, 2012.

D. Jackson, Alloy: a language and tool for exploring software designs, Commun. ACM, vol.62, issue.9, 2019.

S. S. Jongmans and F. Arbab, Overview of thirty semantic formalisms for Reo, Sci. Ann. Comp. Sci, vol.22, issue.1, 2012.

P. Merle, O. Barais, J. Parpaillon, N. Plouzeau, and S. Tata, A precise metamodel for open cloud computing interface, 8th IEEE International Conference on Cloud Computing, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01188800

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

T. Metsch, A. Edmonds, and B. Parak, Open Grid Forum -Open Cloud Computing Interface -Infrastructure, 2016.

T. Metsch and M. Mohamed, Open Grid Forum -Open Cloud Computing Interface -Platform, 2016.

M. M. Moscato, C. G. Lopez-pombo, and M. F. Frias, Dynamite: A tool for the verification of alloy models based on pvs, ACM Trans. on Software Engineering and Methodology, vol.23, issue.2, 2014.

R. Nyren, A. Edmonds, A. Papspyrou, T. Metsch, and B. Parak, Open Grid Forum -Open Cloud Computing Interface -Core, 2016.

A. Schmitt and J. B. Stefani, The Kell Calculus: A Family of Higher-Order Distributed Process Calculi, Global Computing, vol.3267, 2005.

S. Sicard, F. Boyer, and N. Palma, Using Components for Architecture-Based Management: The Self-Repair Case, 30th International Conference on Software Engineering, 2008.

A. Souri, N. J. Navimipour, and A. M. Rahmani, Formal verification approaches and standards in the cloud computing: A comprehensive and systematic review, Computer Standards & Interfaces, vol.58, 2018.

J. B. Stefani, Components as location graphs, 11th Int. Symposium Formal Aspects of Component Software FACS 2014, vol.8997, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01094208

J. B. Stefani and M. Vassor, Encapsulation and sharing in dynamic software architectures: The Hypercell framework, 39th Int. Conf. Formal Techniques for Distributed Objects, Components, and Systems (FORTE), 2019.
URL : https://hal.archives-ouvertes.fr/hal-02313751

M. Wurster, U. Breitenbücher, M. Falkenthal, C. Krieger, F. Leymann et al., The essential deployment metamodel: A systematic review of deployment automation technologies. Software Intensive Cyber-Physical Systems, 2019.

K. Yongsiriwit, M. Sellami, and W. Gaaloul, A semantic framework supporting cloud resource descriptions interoperability, 9th IEEE International Conference on Cloud Computing, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01455119

, Saint Ismier Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria