Projects per year
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 language | English |
---|---|
Pages (from-to) | 881-906 |
Number of pages | 26 |
Journal | International Journal of Computer Mathematics |
Volume | 91 |
Issue number | 5 |
DOIs | |
Publication status | Published - 1 May 2014 |
Externally published | Yes |
Keywords / Materials (for Non-textual outputs)
- 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.Projects
- 1 Finished
-
A14FM : using A1 to aid automation of proof search in formal methods
Bundy, A., Bundy, A., Grov, G., Ireland, A. & Jones, C. B.
1/04/10 → 31/03/14
Project: Research