Formal design of cloud computing systems in maude

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


Cloud computing systems are complex distributed systems whose design is challenging for two main reasons: (1) since they are distributed systems, a correct design is very hard to achieve by testing alone; and (2) cloud computing applications have high availability and performance requirements; but these are hard to measure before implementation and hard to compare between different implementations. This paper summarizes our experience in using formal specification in Maude and model checking analysis to quickly explore the design space of a cloud computing system to achieve a high quality design that: (1) has verified correctness guarantees; (2) has better performance properties than other design alternatives so explored; (3) can be achieved before an actual implementation; and (4) can be used for both rapid prototyping and for automatic code generation.

Original languageEnglish (US)
Title of host publicationFormal Methods
Subtitle of host publicationFoundations and Applications - 21st Brazilian Symposium, SBMF 2018, Proceedings
EditorsTiago Massoni, Mohammad Reza Mousavi
Number of pages15
ISBN (Print)9783030030438
StatePublished - 2018
Event21st Brazilian Symposium on Formal Methods, SBMF 2018 - Salvador, Brazil
Duration: Nov 26 2018Nov 30 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11254 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other21st Brazilian Symposium on Formal Methods, SBMF 2018


  • Cloud computing
  • Maude
  • Rewriting logic
  • Specification and verification of distributed systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Formal design of cloud computing systems in maude'. Together they form a unique fingerprint.

Cite this