The Community for Technology Leaders
RSS Icon
Issue No.01 - {} (2013 vol.1)
pp: 1
Saif U. R. Malik , Dept. of Electr. & Comput. Eng., North Dakota State Univ., Fargo, ND, USA
Samee U. Khan , Dept. of Electr. & Comput. Eng., North Dakota State Univ., Fargo, ND, USA
Sudarshan K. Srinivasan , Dept. of Electr. & Comput. Eng., North Dakota State Univ., Fargo, ND, USA
Virtualization is a key aspect to achieve scalability and flexibility in a cloud. Many solutions have been proposed to monitor and deploy Virtual Machines (VM) in resource pool of cloud. However, most of the cloud management systems, such as Amazon EC2 are proprietary. In the said perspective, many open source VM-based platforms have tossed for general users to research. The existing work has mainly focused on the discussion of architecture, feature-set, and performance analysis. Other important aspects, such as formal analysis, modeling, and verification are usually ignored. In this paper, we provide formal analysis, modeling, and verification of three open source state-of-the-art VM-based cloud platforms: (a) Eucalyptus, (b) Open Nebula, and (c) Nimbus. We used High-Level Petri Nets (HLPN) to model and analyze the structural and behavioral properties of the systems. Moreover, to verify the models, we have used Satisfiability Modulo Theories Library (SMT-Lib) and Z3 Solver. We modeled about 100 VM to verify the correctness and feasibility of our models. The results reveal that the models are functioning correctly. Moreover, the increase in the number of VM does not affect the working of the models that indicates the practicability of the models in a highly scalable and flexible environment.
Virtualization, Analytical models, Software engineering, Computational modeling, IP networks, Computer architecture, Cloud computing,Model checking, Virtualization, Analytical models, Software engineering, Computational modeling, IP networks, Computer architecture, Analysis, Formal methods, Software/Program Verification, Software Engineering, Software/Software Engineering
Saif U. R. Malik, Samee U. Khan, Sudarshan K. Srinivasan, "Modeling and Analysis of State-of-the-art VM-based Cloud Management Platforms", IEEE Transactions on Cloud Computing, vol.1, no. 1, pp. 1, {} 2013, doi:10.1109/TCC.2013.3
[1] R. Buyya, S.Y. Chee, and S. Venugopal, "Market-Oriented Cloud Computing: Vision, Hype, and Reality for Delivering IT Services as Computing Utilities," Proc. IEEE 10th Int'l Conf. High Performance Computing and Comm. (HPCC '08), pp. 5-13, Sept. 2008.
[2] P. Mell and T. Grance, "Definition of Cloud Computing," technical report, NIST, 2009.
[3] E. Keller, J. Szefer, J. Rexford, and R.B. Lee, "NoHype: Virtualized Cloud Infrastructure without the Virtualization," Proc. ACM 37th Ann. Int'l Symp. Computer Architecture (ISCA '10), pp. 350-361, June 2010.
[4] M. Eisen Marcum Technology, Introduction to Virtualization, "The Long Island," Chapter of the IEEE Circuits and Systems (CAS) Soc., Apr. 2011.
[5] A. Vichos, "Agent-Based Management of Virtual Machines for Cloud Infrastructure," Master's thesis, School of Informatics, Univ. of Edinburgh, 2011.
[6] B. Sotomayor, R.S. Montero, I.M. Llorente, and I. Foster, "Capacity Leasing in Cloud Systems Using the OpenNebula Engine," Proc. Workshop Cloud Computing and its Applications (CCA '08), Oct. 2008.
[7] Amazon Elastic Compute Cloud (Amazon EC2), http://aws. amazon.comec2/, 2013.
[8] Google App Engine,, 2013.
[9] Science Clouds, http:/, 2013.
[10] D. Nurmi, R. Wolski, C. Grzegorczyk, G. Obertelli, S. Soman, L. Youseff, and D. Zagorodnov, "The Eucalyptus Open-Source Cloud Computing System," Proc. Ninth IEEE/ACM Int'l Symp. Cluster Computing and the Grid (CCGrid '09), pp. 124-131, May 2009.
[11] oVirt, http://www.ovirt.orgHome, 2013.
[12] Enomaly, http:/, 2013.
[13] F. Panzieri, O. Babaoglu, S. Ferretti, V. Ghini, and M. Marzolla, "Distributed Computing in the 21st Century: Some Aspects of Cloud Computing," Technology-Enhanced Systems and Tools for Collaborative Learning Scaffolding, pp. 393-412, Springer, 2011.
[14] R. Wojtczuk, "Subverting the Xen Hypervisor," Black Hat USA, 2008.
[15] I. Habib, "Virtualization with kVM," Linux Journal, article 8, no. 166, 2008.
[16] D. Cerbelaud, S. Garg, and J. Huylebroeck, "Opening the Clouds: Qualitative Overview of the State-of-the-Art Open Source Vm-Based Cloud Management Platforms," Proc. 10th ACM/IFIP Int'l Conf. Middleware, pp. 1-8, 2009.
[17] P.T. Endo, G.E. Gonçalves, J. Kelner, and D. Sadok, "A Survey on Open-Source Cloud Computing Solutions," Proc. Eighth Workshop Cloud and Grid Applications, pp. 3-16, 2010.
[18] B. Sotomayor, R.S. Montero, I.M. Llorente, and I. Foster, "Virtual Infrastructure Management in Private and Hybrid Clouds," IEEE Internet Computing, vol. 13, no. 5, pp. 14-22, Oct. 2009.
[19] N. Khan, A. Noraziah, E.I. Ismail, and M.M. Deris, "Cloud Computing: Analysis of Various Platforms," J. Entrepreneurship and Innovation, vol. 3, no. 2, pp. 51-59, 2012.
[20] T. Murata, "Petri Nets: Properties, Analysis and Applications," Proc. IEEE, vol. 77, no. 4, pp. 541-580, Apr. 1989.
[21] Lectures on Petri Nets I: Basic Models, W. Reisig and G. Rozenberg, eds., Springer-Verlag, 1998.
[22] S.K. Garg, S. Versteeg, and R. Buyya, "A Framework for Ranking of Cloud Computing Services," Future Generation Computer Systems, vol. 29, no. 4, pp. 1012-1023, 2013.
[23] L. Moura and N. Bjrner, "Satisfiability Modulo Theories: An Appetizer," Formal Methods: Foundations and Applications , pp. 23-36, Springer, 2009.
[24] B. Javadi, R. Thulasiram, and R. Buyya, "Characterizing Spot Price Dynamics in Public Cloud Environments," Future Generation Computer Systems, vol. 29, no. 4, pp. 988-999, 2013.
[25] OpenStack, , 2013.
[26] M. Frade and J.S. Pinto, "Verification Conditions for Source-Level Imperative Programs," Technical Report DI-CCTC-08-01, Univ. of Minho, 2008.
[27] SMT-Lib http:/, 2013.
[28] S.U.R. Malik, S.K. Srinivasan, S.U. Khan, and L. Wang, "A Methodology for OSPF Routing Protocol Verification," Proc. 12th Int'l Conf. Scalable Computing and. Comm. (ScalCom '12), Dec. 2012.
[29] G. von Laszewski, J. Diaz, F. Wang, and G.C. Fox, "Comparison of Multiple Cloud Frameworks," Proc. IEEE Conf. Cloud Computing, pp. 734-741, 2012.
[30] L. de Moura and N. Bjorner, "Z3: An Efficient SMT Solver," Proc. Theory and practice of software, 14th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08), 2008.
[31] L. Cordeiro, B. Fischer, and J. Marques-Silva, "SMT-Based Bounded Model Checking for Embedded ANSI-C Software," Proc. IEEE/ACM Int'l Conf. Automated Software Eng. (ASE '09), pp. 137-148, 2009.
[32] M. Rosenblum and T. Garfinkel, "Virtual Machine Monitors: Current Technology and Future Trends," Computer, vol. 38, no. 5, pp. 39-47, May 2005.
[33] Y. Li and O. Boucelma, "A CPN Provenance Model of Workflow: Towards Diagnosis in the Cloud," Proc. Conf. Advances in Databases and Information Systems, pp. 55-64, 2011.
[34] P. Sempolinski and D. Thain, "A Comparison and Critique of Eucalyptus, OpenNebula and Nimbus," Proc. IEEE Second Int'l Conf. Cloud Computing Technology and Science (CloudCom '10), pp. 417-426, 2010.
[35] D. Nurmi, R. Wolski, C. Grzegorczyk, G. Obertelli, S. Soman, L. Youseff, and D. Zagorodnov, "The Eucalyptus Open-Source Cloud-Computing System," Proc. IEEE Int'l Symp. Cluster Computing and the Grid, pp. 124-131, 2009.
[36] Eucalyptus Systems Home Page, http:/, 2013.
[37] J. Xu, M. Zhao, J. Fortes, R. Carpenter, and M. Yousif, "Autonomic Resource Management in Virtualized Data Centers Using Fuzzy Logic-Based Approaches," J. Cluster Computing, vol. 11, pp. 213-227, 2008.
[38] D. Milojicic, I.M. Llorente, and R.S. Montero, "OpenNebula: A Cloud Management Tool," IEEE Internet Computing, vol. 15, no. 2, pp. 11-14, Mar./Apr. 2011.
[39] Open Nebula, http:/, 2013.
[40] Nimbus,, 2013.
[41] I. Foster and C. Kesselman, "The Globus Project: A Status Report," Proc. IEEE Heterogeneous Computing Workshop, pp. 4-18, 1998.
[42] A Survey of Open-Source Cloud Infrastructure Using FutureGrid Testbed, T. Wu, S.N. Baasha, and S.S. Karwa, http://salsahpc. , 2013.
[43] P. Campegiani and F.L. Presti, "A General Model for Virtual Machines Resources Allocation in Multi-Tier Distributed Systems," Proc. Int'l Conf. Autonomic and Autonomous Systems, pp. 162-167, 2009.
[44] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu, "Bounded Model Checking," Advances in Computers, vol. 58, Academic press, 2003.
[45] Y.M. Quemener and T. Jeron, "Model Checking of CL on Infinite Kripke Structures Defined by Simple Grammers," Technical Report RR-2563, 1995.
[46] M. Maidl, "The Common Fragment of CTL and LTL," Proc. IEEE Symp. Foundations of Computer Science, 2000.
[47] F. Zhang, J. Chen, H. Chen, and B. Zang, "CloudVisor: Retrofitting Protection of Virtual Machines in Multi-Tenant Cloud with Nested Virtualization," Proc. 23rd ACM Symp. Operating Systems Principles (SOSP '11), Oct. 2011.
[48] Z. Wang and X. Jiang, "HyperSafe: A Lightweight Approach to Provide Lifetime Hypervisor Control-Flow Integrity," Proc. IEEE Symp. Security and Privacy (SP '10), pp. 380-395, 2010.
[49] F. Sabahi, "Secure Virtualization for Cloud Environment Using Hypervisor-Based Technology," Int'l J. Machine Learning and Computing, vol. 2, no. 1, pp. 39-45, Feb. 2012.
[50] S.U.R. Malik, S.K. Srinivasan, and S.U. Khan, "Convergence Time Analysis of Open Shortest Path First Routing Protocol in Internet Scale Networks," IET Electronics Letters, vol. 48, no. 19, pp. 1188-1190, 2012.
[51] J. Kolodiej, S.U. Khan, E. Gelenbe, and E.-G. Talbi, "Scalable Optimization in Grid, Cloud, and Intelligent Network Computing," Concurrency and Computation: Practice and Experience, vol. 25, no. 12, pp. 1719-1721, 2013.
71 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool