{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T01:56:17Z","timestamp":1790819777670,"version":"4.1.0"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319254227","type":"print"},{"value":"9783319254234","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25423-4_3","type":"book-chapter","created":{"date-parts":[[2015,11,30]],"date-time":"2015-11-30T12:10:46Z","timestamp":1448885446000},"page":"33-49","source":"Crossref","is-referenced-by-count":9,"title":["Formalization and Verification of Declarative Cloud Orchestration"],"prefix":"10.1007","author":[{"given":"Hiroyuki","family":"Yoshida","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,12,1]]},"reference":[{"key":"3_CR1","unstructured":"Amazon Web Services: AWS CloudFormation: Configuration Management & Cloud Orchestration. \n                    http:\/\/aws.amazon.com\/cloudformation\/\n                    \n                  . Accessed 03 April 2015"},{"key":"3_CR2","unstructured":"Ansible: Ansible is Simple IT Automation. \n                    http:\/\/www.ansible.com\/home\/\n                    \n                  . Accessed 03 April 2015"},{"key":"3_CR3","unstructured":"CafeOBJ (2014). \n                    http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"3_CR4","unstructured":"Chef Software: IT automation for speed and awesomeness. \n                    https:\/\/www.chef.io\/chef\/\n                    \n                  . Accessed 03 April 2015"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Etchevers, X., Coupaye, T., Boyer, F., Palma, N.D.: Self-configuration of distributed applications in the cloud. In: IEEE CLOUD, pp. 668\u2013675 (2011)","DOI":"10.1109\/UCC.2011.32"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-15545-6_13","volume-title":"Software, Services, and Systems","author":"K Futatsugi","year":"2015","unstructured":"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\u2013192. Springer, Heidelberg (2015)"},{"key":"3_CR7","unstructured":"OASIS: TOSCA - Topology and Orchestration Specification for Cloud Applications Version 1.0. \n                    http:\/\/docs.oasis-open.org\/tosca\/TOSCA\/v1.0\/os\/TOSCA-v1.0-os.pdf\n                    \n                  . Accessed 03 April 2015"},{"key":"3_CR8","unstructured":"OBJ (2003). \n                    http:\/\/cseweb.ucsd.edu\/goguen\/sys\/obj.html"},{"key":"3_CR9","unstructured":"OBJ3 (2005). \n                    http:\/\/www.kindsoftware.com\/products\/opensource\/obj3\/"},{"key":"3_CR10","unstructured":"OpenStack.org: Heat - OpenStack Orchestration. \n                    https:\/\/wiki.openstack.org\/wiki\/Heat\/\n                    \n                  . Accessed 03 April 2015"},{"key":"3_CR11","unstructured":"Puppet Labs: IT Automation Software for System Administrators. \n                    https:\/\/puppetlabs.com\/\n                    \n                  . Accessed 03 April 2015"},{"issue":"2","key":"3_CR12","first-page":"105","volume":"9","author":"G Sala\u00fcn","year":"2013","unstructured":"Sala\u00fcn, 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\u2013117 (2013)","journal-title":"ISSE"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-36249-1_3","volume-title":"Assurances for Self-Adaptive Systems","author":"G Sala\u00fcn","year":"2013","unstructured":"Sala\u00fcn, G., Etchevers, X., De Palma, N., Boyer, F., Coupaye, T.: Verification of a self-configuration protocol for distributed applications in the cloud. In: C\u00e1mara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds.) Assurances for Self-Adaptive Systems. LNCS, vol. 7740, pp. 60\u201379. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25423-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:00:56Z","timestamp":1559314856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25423-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319254227","9783319254234"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25423-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}