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/Published conference outputConference publication


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)
Number of pages15
ISBN (Electronic)978-3-642-34188-5
ISBN (Print)978-3-642-34187-8
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
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference7th International Haifa Verification Conference, HVC 2011
Country/TerritoryUnited Kingdom


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


Dive into the research topics of 'Specification and quantitative analysis of probabilistic cloud deployment patterns'. Together they form a unique fingerprint.

Cite this