@inproceedings{82d06edc37be42f8bf0464bf605b2537,
title = "Formal design of cloud computing systems in maude",
abstract = "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.",
keywords = "Cloud computing, Maude, Rewriting logic, Specification and verification of distributed systems",
author = "Jos{\'e} Meseguer",
year = "2018",
month = jan,
day = "1",
doi = "10.1007/978-3-030-03044-5_2",
language = "English (US)",
isbn = "9783030030438",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag Berlin Heidelberg",
pages = "5--19",
editor = "Tiago Massoni and Mousavi, {Mohammad Reza}",
booktitle = "Formal Methods",
note = "21st Brazilian Symposium on Formal Methods, SBMF 2018 ; Conference date: 26-11-2018 Through 30-11-2018",
}