TY - GEN
T1 - Design and analysis of cloud-based architectures with KLAIM and Maude
AU - Wirsing, Martin
AU - Eckhardt, Jonas
AU - Mühlbauer, Tobias
AU - Meseguer, José
N1 - Funding Information:
This work has been partially sponsored by the EU-funded projects FP7-257414 ASCENS and FP7-256980 NESSoS, and AFOSR Grant FA8750-11-2-0084.
PY - 2012
Y1 - 2012
N2 - Cloud computing is a modern paradigm for offering and utilizing distributed infrastructure resources in a dynamic way. Cloud-based systems are safety- and security-critical; they need to satisfy time-critical performance-based quality of service properties and to dynamically adapt to changes in the potentially hostile and uncertain environment they operate in. In this paper we propose the coordination language KLAIM and a composite actor approach for modelling Cloud-based architectures whereas for formally analyzing such architectures we use a rewritingbased approach. We specify the operational semantics of KLAIM in Maude, show how to realize KLAIM programs in a distributed implementation of Maude, and simulate and analyze three simple Cloud architectures with Maude and the Maude LTL model checker. Moreover, we report shortly on the Maude specification and analysis of three larger Cloud case studies using the composite actor model, where statistical model checking with the Maude-based tool PVeStA is successfully used for detecting bugs and performance issues and for analyzing a defense mechanism against distributed denial-of-service attacks.
AB - Cloud computing is a modern paradigm for offering and utilizing distributed infrastructure resources in a dynamic way. Cloud-based systems are safety- and security-critical; they need to satisfy time-critical performance-based quality of service properties and to dynamically adapt to changes in the potentially hostile and uncertain environment they operate in. In this paper we propose the coordination language KLAIM and a composite actor approach for modelling Cloud-based architectures whereas for formally analyzing such architectures we use a rewritingbased approach. We specify the operational semantics of KLAIM in Maude, show how to realize KLAIM programs in a distributed implementation of Maude, and simulate and analyze three simple Cloud architectures with Maude and the Maude LTL model checker. Moreover, we report shortly on the Maude specification and analysis of three larger Cloud case studies using the composite actor model, where statistical model checking with the Maude-based tool PVeStA is successfully used for detecting bugs and performance issues and for analyzing a defense mechanism against distributed denial-of-service attacks.
KW - cloud computing
KW - composite actor model
KW - coordination languages
KW - distributed systems
KW - formal analysis
KW - rewriting logic
UR - http://www.scopus.com/inward/record.url?scp=84868323574&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84868323574&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-34005-5_4
DO - 10.1007/978-3-642-34005-5_4
M3 - Conference contribution
AN - SCOPUS:84868323574
SN - 9783642340048
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 54
EP - 82
BT - Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers
T2 - 9th International Workshop on Rewriting Logic and Its Applications, WRLA 2012, Held as a Satellite Event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
Y2 - 24 March 2012 through 25 March 2012
ER -