Issue No.02 - March-April (2013 vol.15)
pp: 36-41
Shinji Kikuchi , Fujitsu Laboratories Ltd., Japan
Yasuhide Matsumoto , Fujitsu Laboratories Ltd., Japan
Server virtualization technologies and their live migration function support more efficient use of computing resources in cloud datacenters. However, many management operations for virtual machines can be evoked simultaneously in large-scale systems. What happens if many live migrations are executed simultaneously?
Computational modeling, Servers, Probabilistic logic, Cloud computing, Analytical models, Receivers, Logic gates, Virtualization, model checking, system management operations, virtual machine, operation performance, cloud computing, datacenter, live migration, formal methods
Shinji Kikuchi, Yasuhide Matsumoto, "Using Model Checking to Evaluate Live Migrations", IT Professional, vol.15, no. 2, pp. 36-41, March-April 2013, doi:10.1109/MITP.2012.45
1. M. Armbrust et al., Above the Clouds: A Berkeley View of Cloud Computing, tech. report UCB/EECS-2009-28, Electrical Engineering and Computer Sciences Dept., University of California, Berkley, 2009.
2. C. Clark et al., "Live Migration of Virtual Machines," Proc. 2nd ACM/Usenix Symp. Network Systems Design and Implementation, Usenix, 2005, pp. 273–286.
3. V. Soundararajan and J.M. Anderson, "The Impact of Management Operations on the Virtualized Datacenter," Proc. 37th Ann. Int'l Symp. Computer Architecture (ICSA 10), ACM, 2010, pp. 326–337.
4. S. Kikuchi and Y. Matsumoto, "What Will Happen if Cloud Management Operations Burst Out?" Proc. 12th IFIP/IEEE Int'l Symp. Integrated Network Management (IM 11), IEEE, 2011, pp. 97–104.
5. E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT Press, 1999.
6. M. Ben-Ari, Z. Manna, and A. Pnueli, "The Temporal Logic of Branching Time," Acta Informatica 20, vol. 20, no. 3, 1983, pp. 207–226.
7. A. Pnueli, "The Temporal Logic of Programs," Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS 77), IEEE CS, 1977, pp. 46–57.
8. R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Transactions on Computers, vol. C-35, no. 8, 1986, pp. 677–691.
9. M. Kwiatkowska, G. Norman, and D. Parker, "Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach," Int'l J. Software Tools for Technology Transfer, vol. 6, no. 2, 2004, pp. 128–142.
10. M. Kwiatkowska, G. Norman, and D. Parker, "Quantitative Analysis with the Probabilistic Model Checker PRISM," Electronic Notes in Theoretical Computer Science, vol. 153, no. 2, 2005, pp. 5–31.
11. R. Calinescu, S. Kikuchi, and M. Kwiatkowska, "Formal Methods for the Development and Verification of Autonomic IT Systems," Formal and Practical Aspects of Autonomic Computing and Networking: Specification, Development and Verification, IGI Global, 2011.
12. R. Murch, Autonomic Computing, IBM Press, 2004.
13. K. Kaori and T. Katayama, "An Analysis of M/G/1 Queuing Model with Gated Vacations by the Level-Crossing Method," Bull. Toyama Prefectural Univ., no. 18, 2008, pp. 42–49 (in Japanese).
14. S. Kikuchi and Y. Matsumoto, "Performance Modeling of Concurrent Live Migration Operations in Cloud Computing Systems Using PRISM Probabilistic Model Checker," Proc. 2011 IEEE Int'l Conf. Cloud Computing (Cloud 11), IEEE, 2011, pp. 49–56.