Specification and quantitative analysis of probabilistic cloud deployment patterns

Kenneth Johnson*, Simon Reed, Radu Calinescu

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Cloud computing is a new technological paradigm offering computing infrastructure, software and platforms as a pay-as-you-go, subscription-based service. Many potential customers of cloud services require essential cost assessments to be undertaken before transitioning to the cloud. Current assessment techniques are imprecise as they rely on simplified specifications of resource requirements that fail to account for probabilistic variations in usage. In this paper, we address these problems and propose a new probabilistic pattern modelling (PPM) approach to cloud costing and resource usage verification. Our approach is based on a concise expression of probabilistic resource usage patterns translated to Markov decision processes (MDPs). Key costing and usage queries are identified and expressed in a probabilistic variant of temporal logic and calculated to a high degree of precision using quantitative verification techniques. The PPM cost assessment approach has been implemented as a Java library and validated with a case study and scalability experiments.

Original languageEnglish
Title of host publicationHardware and software : verification and testing
Subtitle of host publication7th international Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, revised selected papers
EditorsKerstin Eder, João Lourenço, Onn Shehory
Place of PublicationBerlin (DE)
PublisherSpringer
Pages145-159
Number of pages15
ISBN (Electronic)978-3-642-34188-5
ISBN (Print)978-3-642-34187-8
DOIs
Publication statusPublished - 2012
Event7th International Haifa Verification Conference, HVC 2011 - Haifa, United Kingdom
Duration: 6 Dec 20118 Dec 2011

Publication series

NameLecture notes in computer science
PublisherSpringer
Volume7261
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Haifa Verification Conference, HVC 2011
CountryUnited Kingdom
CityHaifa
Period6/12/118/12/11

Fingerprint

Quantitative Analysis
Specification
Specifications
Temporal logic
Cloud computing
Chemical analysis
Scalability
Costs
Resources
Markov Decision Process
Temporal Logic
Cloud Computing
Modeling
Experiments
Java
Customers
Infrastructure
Paradigm
Query
Software

Keywords

  • Cloud computing
  • costing analysis
  • formal modelling and specification
  • formal specification languages
  • formal verification methods
  • Markov processes
  • probabilistic model checking
  • resource usage patterns

Cite this

Johnson, K., Reed, S., & Calinescu, R. (2012). Specification and quantitative analysis of probabilistic cloud deployment patterns. In K. Eder, J. Lourenço, & O. Shehory (Eds.), Hardware and software : verification and testing: 7th international Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, revised selected papers (pp. 145-159). (Lecture notes in computer science; Vol. 7261). Berlin (DE): Springer. https://doi.org/10.1007/978-3-642-34188-5_14
Johnson, Kenneth ; Reed, Simon ; Calinescu, Radu. / Specification and quantitative analysis of probabilistic cloud deployment patterns. Hardware and software : verification and testing: 7th international Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, revised selected papers. editor / Kerstin Eder ; João Lourenço ; Onn Shehory. Berlin (DE) : Springer, 2012. pp. 145-159 (Lecture notes in computer science).
@inproceedings{11932bdfb9214bb1bf9c0b5c9691c69b,
title = "Specification and quantitative analysis of probabilistic cloud deployment patterns",
abstract = "Cloud computing is a new technological paradigm offering computing infrastructure, software and platforms as a pay-as-you-go, subscription-based service. Many potential customers of cloud services require essential cost assessments to be undertaken before transitioning to the cloud. Current assessment techniques are imprecise as they rely on simplified specifications of resource requirements that fail to account for probabilistic variations in usage. In this paper, we address these problems and propose a new probabilistic pattern modelling (PPM) approach to cloud costing and resource usage verification. Our approach is based on a concise expression of probabilistic resource usage patterns translated to Markov decision processes (MDPs). Key costing and usage queries are identified and expressed in a probabilistic variant of temporal logic and calculated to a high degree of precision using quantitative verification techniques. The PPM cost assessment approach has been implemented as a Java library and validated with a case study and scalability experiments.",
keywords = "Cloud computing, costing analysis, formal modelling and specification, formal specification languages, formal verification methods, Markov processes, probabilistic model checking, resource usage patterns",
author = "Kenneth Johnson and Simon Reed and Radu Calinescu",
year = "2012",
doi = "10.1007/978-3-642-34188-5_14",
language = "English",
isbn = "978-3-642-34187-8",
series = "Lecture notes in computer science",
publisher = "Springer",
pages = "145--159",
editor = "Kerstin Eder and Jo{\~a}o Louren{\cc}o and Onn Shehory",
booktitle = "Hardware and software : verification and testing",
address = "Germany",

}

Johnson, K, Reed, S & Calinescu, R 2012, Specification and quantitative analysis of probabilistic cloud deployment patterns. in K Eder, J Lourenço & O Shehory (eds), Hardware and software : verification and testing: 7th international Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, revised selected papers. Lecture notes in computer science, vol. 7261, Springer, Berlin (DE), pp. 145-159, 7th International Haifa Verification Conference, HVC 2011, Haifa, United Kingdom, 6/12/11. https://doi.org/10.1007/978-3-642-34188-5_14

Specification and quantitative analysis of probabilistic cloud deployment patterns. / Johnson, Kenneth; Reed, Simon; Calinescu, Radu.

Hardware and software : verification and testing: 7th international Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, revised selected papers. ed. / Kerstin Eder; João Lourenço; Onn Shehory. Berlin (DE) : Springer, 2012. p. 145-159 (Lecture notes in computer science; Vol. 7261).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Specification and quantitative analysis of probabilistic cloud deployment patterns

AU - Johnson, Kenneth

AU - Reed, Simon

AU - Calinescu, Radu

PY - 2012

Y1 - 2012

N2 - Cloud computing is a new technological paradigm offering computing infrastructure, software and platforms as a pay-as-you-go, subscription-based service. Many potential customers of cloud services require essential cost assessments to be undertaken before transitioning to the cloud. Current assessment techniques are imprecise as they rely on simplified specifications of resource requirements that fail to account for probabilistic variations in usage. In this paper, we address these problems and propose a new probabilistic pattern modelling (PPM) approach to cloud costing and resource usage verification. Our approach is based on a concise expression of probabilistic resource usage patterns translated to Markov decision processes (MDPs). Key costing and usage queries are identified and expressed in a probabilistic variant of temporal logic and calculated to a high degree of precision using quantitative verification techniques. The PPM cost assessment approach has been implemented as a Java library and validated with a case study and scalability experiments.

AB - Cloud computing is a new technological paradigm offering computing infrastructure, software and platforms as a pay-as-you-go, subscription-based service. Many potential customers of cloud services require essential cost assessments to be undertaken before transitioning to the cloud. Current assessment techniques are imprecise as they rely on simplified specifications of resource requirements that fail to account for probabilistic variations in usage. In this paper, we address these problems and propose a new probabilistic pattern modelling (PPM) approach to cloud costing and resource usage verification. Our approach is based on a concise expression of probabilistic resource usage patterns translated to Markov decision processes (MDPs). Key costing and usage queries are identified and expressed in a probabilistic variant of temporal logic and calculated to a high degree of precision using quantitative verification techniques. The PPM cost assessment approach has been implemented as a Java library and validated with a case study and scalability experiments.

KW - Cloud computing

KW - costing analysis

KW - formal modelling and specification

KW - formal specification languages

KW - formal verification methods

KW - Markov processes

KW - probabilistic model checking

KW - resource usage patterns

UR - http://www.scopus.com/inward/record.url?scp=84868103092&partnerID=8YFLogxK

UR - http://link.springer.com/chapter/10.1007%2F978-3-642-34188-5_14

U2 - 10.1007/978-3-642-34188-5_14

DO - 10.1007/978-3-642-34188-5_14

M3 - Conference contribution

AN - SCOPUS:84868103092

SN - 978-3-642-34187-8

T3 - Lecture notes in computer science

SP - 145

EP - 159

BT - Hardware and software : verification and testing

A2 - Eder, Kerstin

A2 - Lourenço, João

A2 - Shehory, Onn

PB - Springer

CY - Berlin (DE)

ER -

Johnson K, Reed S, Calinescu R. Specification and quantitative analysis of probabilistic cloud deployment patterns. In Eder K, Lourenço J, Shehory O, editors, Hardware and software : verification and testing: 7th international Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, revised selected papers. Berlin (DE): Springer. 2012. p. 145-159. (Lecture notes in computer science). https://doi.org/10.1007/978-3-642-34188-5_14