Visualisation and Automated Formal Verification of <scp>TOSCA</scp> Workflows

ABSTRACT Background Topology and Orchestration Specification for Cloud Applications (TOSCA) is a specification language used for modelling topology and orchestration of cloud applications. This language particularly allows the description of workflows that can be used for specifying management tasks such as (un)deployment plans. Motivations This textual language for describing TOSCA workflows does not provide any visual notation for graphically designing or observing the corresponding workflows. Moreover, this specification language is error‐prone and can be source of mistakes during the writing of the management plans. Methods In this article, we propose a transformation from TOSCA to the graphical Business Process Model and Notation (BPMN), which allows the visualisation of TOSCA workflows. We also provide automated verification techniques for analysing TOSCA (un)deployment workflows in terms of functional and architectural properties as well as execution times. The transformation and verification steps are achieved in a fully automated way. Results This approach computes BPMN models and verification results within a reasonable time on realistic applications.