Formalization and Verification of Declarative Cloud Orchestration.

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.