Title :
Towards Formal Modeling and Verification of Cloud Architectures: A Case Study on Hadoop
Author :
Reddy, G. Shrikanth ; Yuzhang Feng ; Yang Liu ; Jin Song Dong ; Sun Jun ; Kanagasabai, Rajaraman
Author_Institution :
Oracle India Private Ltd., Bangalore, India
fDate :
June 28 2013-July 3 2013
Abstract :
Hadoop is a popular open source implementation of MapReduce, that has a number of prominent users including Yahoo!, Facebook, and Twitter. Though several works have focused on deploying algorithms on Hadoop MapReduce, research efforts into applying formal methods to prove the correctness of hadoop systems are limited. In this paper we propose a holistic approach to verify the correctness of hadoop systems using model checking techniques. We model Hadoop´s parallel architecture to constraint it to valid start up ordering and identify and prove the benefits of data locality, deadlock-freeness and non-termination among others.
Keywords :
cloud computing; formal verification; parallel processing; public domain software; Hadoop MapReduce; Hadoop parallel architecture; MapReduce; cloud architectures; data locality; deadlock-freeness; formal modeling; formal verification; model checking techniques; open source implementation; Algebra; Computational modeling; Computer architecture; Data models; Electronic mail; Model checking; System recovery; Formal Verification; Hadoop;
Conference_Titel :
Services (SERVICES), 2013 IEEE Ninth World Congress on
Conference_Location :
Santa Clara, CA
Print_ISBN :
978-0-7695-5024-4
DOI :
10.1109/SERVICES.2013.47
