Abstract
Automation of cloud system operations, for example, which set up, monitor, and back up such systems, is called Cloud Orchestration. A standard specification language, TOSCA (Topology and Orchestration Specification for Cloud Applications), has been proposed to define topologies of cloud applications. A topology is a static structure of resources, such as VMs and software components, and a TOSCA conforming tool is expected to automate system operations based on the topologies. The current TOSCA standard, however, does not yet explicitly provide any way to formally define behavior of a topology (how to automate a topology). This paper proposes how to specify behavior of TOSCA topologies as state transition systems and to verify that orchestrated operations always successfully complete by proving the transition systems enjoys leads-to (a class of liveness) properties. We report on a case study in which we have specified and verified a setup operation to demonstrate the feasibility and usefulness of the proposed solution.
This work was supported in part by Grant-in-Aid for Scientific Research (S) 23220002 from Japan Society for the Promotion of Science (JSPS).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Amazon Web Services: AWS CloudFormation: Configuration Management & Cloud Orchestration. http://aws.amazon.com/cloudformation/. Accessed 03 April 2015
Ansible: Ansible is Simple IT Automation. http://www.ansible.com/home/. Accessed 03 April 2015
CafeOBJ (2014). http://www.ldl.jaist.ac.jp/cafeobj/
Chef Software: IT automation for speed and awesomeness. https://www.chef.io/chef/. Accessed 03 April 2015
Etchevers, X., Coupaye, T., Boyer, F., Palma, N.D.: Self-configuration of distributed applications in the cloud. In: IEEE CLOUD, pp. 668–675 (2011)
Futatsugi, K.: Generate & check method for verifying transition systems in CafeOBJ. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 171–192. Springer, Heidelberg (2015)
OASIS: TOSCA - Topology and Orchestration Specification for Cloud Applications Version 1.0. http://docs.oasis-open.org/tosca/TOSCA/v1.0/os/TOSCA-v1.0-os.pdf. Accessed 03 April 2015
OBJ (2003). http://cseweb.ucsd.edu/goguen/sys/obj.html
OBJ3 (2005). http://www.kindsoftware.com/products/opensource/obj3/
OpenStack.org: Heat - OpenStack Orchestration. https://wiki.openstack.org/wiki/Heat/. Accessed 03 April 2015
Puppet Labs: IT Automation Software for System Administrators. https://puppetlabs.com/. Accessed 03 April 2015
Salaün, G., Boyer, F., Coupaye, T., Palma, N.D., Etchevers, X., Gruber, O.: An experience report on the verification of autonomic protocols in the cloud. ISSE 9(2), 105–117 (2013)
Salaün, G., Etchevers, X., De Palma, N., Boyer, F., Coupaye, T.: Verification of a self-configuration protocol for distributed applications in the cloud. In: Cámara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds.) Assurances for Self-Adaptive Systems. LNCS, vol. 7740, pp. 60–79. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Yoshida, H., Ogata, K., Futatsugi, K. (2015). Formalization and Verification of Declarative Cloud Orchestration. In: Butler, M., Conchon, S., Zaïdi, F. (eds) Formal Methods and Software Engineering. ICFEM 2015. Lecture Notes in Computer Science(), vol 9407. Springer, Cham. https://doi.org/10.1007/978-3-319-25423-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-25423-4_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25422-7
Online ISBN: 978-3-319-25423-4
eBook Packages: Computer ScienceComputer Science (R0)