Formal verification of cloud orchestration design with TOSCA and BPEL

Cloud orchestration helps arrange and coordinate the business processes or workflows to obtain the ultimate and efficient virtual computing resources management. The cloud orchestration standards are introduced to guide the development of the orchestration tools. TOSCA is an important new open cloud standard, introduced and approved by OASIS. Using TOSCA, the cloud providers are able to define the interoperable description of services and their relationships, and to enable the portability and automated management across cloud platforms and infrastructures. However the verification of the cloud orchestration design with TOSCA is still crucial to ensure and alert when the safety properties of the cloud design are violated. We propose an alternative mean to do the formal verification of the cloud orchestration design by superimposing the relevant BPEL of web services over the existing TOSCA description of a cloud orchestration. The resulting formal model of the superimposition between BPEL and TOSCA defines not only the orchestration of the web services but also their service interfaces and the corresponding high level behaviors of the services. In this paper, the safety properties of the cloud orchestration are focused only and defined using the linear temporal logic formula. Our formal model is correctly written in Promela and formally verified using model checker SPIN.