Edinburgh Research Explorer

Formalizing Workflows Partitioning over Federated Clouds: Multi-level Security and Costs

Research output: Contribution to journalArticle

Original languageEnglish
Pages (from-to)881-906
Number of pages26
JournalInternational Journal of Computer Mathematics
Volume91
Issue number5
DOIs
Publication statusPublished - 1 May 2014
Externally publishedYes

Abstract

This paper presents an formalization of federated cloud workflows using the Z notation. It is an abstract specification with properties of interest being observed by the possible deployments, which are symbolically calculated by the Z/EVES theorem prover. Mathematical rules are used to define these properties by restricting valid options for security, cost, dependability, etc. A Haskell implementation of these proved properties is also presented. We have a Haskell implementation of the approach that is used to generate valid workflow deployment options, given the user workflow input and the security and cost properties of interest. The result is a set of (sub)-workflows as GraphWiz files respecting these properties.

    Research areas

  • Bell--LaPadula, Haskell, Z/EVES, federated clouds, formal proof

ID: 22271990