@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",
note = "Funding Information: As the references make clear, most these ideas have been developed in joint work with a large number of collaborators and former or present students, including: Musab AlTurki, Rakesh Bobba, Jonas Eckhardt, Jatin Ganhotra, Jon Grov, Indranil Gupta, Si Liu, Tobias M{\"u}hlbauer, Son Nguyen, Peter Csaba {\"O}lveczky, Muntasir Raihan Rahman, Stephen Skeirik, and Martin Wirsing. Furthermore, in some of the work I report on, such as [19, 20, 35], I have not been involved. These projects were partially supported by the Air Force Research Laboratory and the Air Force Office of Scientific Research, under agreement number FA8750-11-2-0084, the National Science Foundation under Grant Nos. NSF CNS 1409416 and NSF CNS 1319527, and the Naval Research Laboratory under contract number NRL N00173-17-1-G002. I thank the organizers of SBMF 2018 for giving me the opportunity of presenting these ideas at the meeting in Salvador. Funding Information: Acknowledgements. As the references make clear, most these ideas have been developed in joint work with a large number of collaborators and former or present students, including: Musab AlTurki, Rakesh Bobba, Jonas Eckhardt, Jatin Ganhotra, Jon Grov, Indranil Gupta, Si Liu, Tobias M{\"u}hlbauer, Son Nguyen, Peter Csaba {\"O}lveczky, Muntasir Raihan Rahman, Stephen Skeirik, and Martin Wirsing. Furthermore, in some of the work I report on, such as [19,20,35], I have not been involved. These projects were partially supported by the Air Force Research Laboratory and the Air Force Office of Scientific Research, under agreement number FA8750-11-2-0084, the National Science Foundation under Grant Nos. NSF CNS 1409416 and NSF CNS 1319527, and the Naval Research Laboratory under contract number NRL N00173-17-1-G002. I thank the organizers of SBMF 2018 for giving me the opportunity of presenting these ideas at the meeting in Salvador. Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2018.; 21st Brazilian Symposium on Formal Methods, SBMF 2018 ; Conference date: 26-11-2018 Through 30-11-2018",
year = "2018",
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",
pages = "5--19",
editor = "Tiago Massoni and Mousavi, {Mohammad Reza}",
booktitle = "Formal Methods",
address = "Germany",
}