@Inproceedings{AnalysisCloud@WRLA'12,
   status = {public},
   task = {T7.2},
   publisher = {Springer},
   doi = {10.1007/978-3-642-34005-5_4},
   booktitle = {Proceedings of the 9th International Workshop on Rewriting Logicand its Applications (WRLA 2012)},
   joint-pub = {false},
   series = {LNCS},
   year = {2012},
   invited = {no},
   timestamp = {2012.10.31},
   volume = {7571},
   main = {yes},
   title = {{Design and Analysis of Cloud-Based Architectures with KLAIM andMaude}},
   author = {Martin Wirsing and Jonas Eckhardt and Tobias M\"{u}lbauer and Jos\'{e} Meseguer},
   period = {year2},
   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 systems; 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. These aspects make distributed Cloud-based systems complex and hard to design, build, test, and verify. In this paper we propose the coordination language KLAIM for modelling cloud-based architectures whereas for formally analysing such architectures we use a rewritingbased approach. KLAIM is a process algebrabased formalism for designing distributed applications with (object-oriented) mobile code. It supports explicit localities and multiple tuple spaces and permits exchanging data and processes and retrieving information over the net. As examples for the design of cloud-based architectures in KLAIM we present a simple (Fibonacci-) server consumer application, a load balancing algorithm, a mutual exclusion algorithm and a defense mechanism against denial-of-service attacks. For analysing KLAIM specifications we specify KLAIM in object-oriented Maude and then show how to realize distributed KLAIM programs by providing multiple instances of Maude which communicate via sockets. Then we use the Maude system, the Maude LTL modelchecker and the statistical model checker PVeStA for simulating the cloud computing examples and for verifying appropriate correctness properties.},
   owner = {kroiss},
   accessible = {true},
   partner = {LMU},
   ascens_ref = {true},
   wp = {WP7},
   pages = {54 - 82}
}