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

Leo Freitas, Paul Watson

Research output: Contribution to journalArticlepeer-review

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.
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

Keywords

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

Fingerprint

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