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

Leo Freitas, Paul Watson

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Pages (from-to)881-906
Number of pages26
JournalInternational Journal of Computer Mathematics
Issue number5
Publication statusPublished - 1 May 2014
Externally publishedYes

Keywords / Materials (for Non-textual outputs)

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


Dive into the research topics of 'Formalizing Workflows Partitioning over Federated Clouds: Multi-level Security and Costs'. Together they form a unique fingerprint.

Cite this