Paper Info
Title
Design and analysis of cloud-based architectures with KLAIM and maude
Abstract
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.
Year
DOI
Venue
2012
10.1007/978-3-642-34005-5_4
WRLA
Keywords
Field
DocType
maude specification,coordination language klaim,cloud-based architecture,composite actor model,composite actor approach,klaim program,cloud-based system,larger cloud case study,maude ltl model checker,statistical model checking,cloud computing,rewriting logic,distributed systems
Operational semantics,Programming language,Model checking,Computer science,Statistical model checking,Quality of service,Rewriting,Actor model,Coordination language,Cloud computing
Conference
Citations 
PageRank 
References 
8
0.46
20
Authors
4
Name
Order
Citations
PageRank
Martin Wirsing12158267.89
Jonas Eckhardt2969.24
Tobias Mühlbauer321712.21
José Meseguer49533805.39