臺灣博碩士論文加值系統

隨著科技的發展，公司企業的資料量日益龐大，進而發展出新的“雲端運算”、 “巨量資料” 概念，以及結合兩者使用的雲端運算作巨量資料分析的商機。Hadoop用在雲端運算系統的架設是非常熱門的，有許多雲端運算系統採用Hadoop作為實行之方法。其中，MapReduce框架為Hadoop進行巨量資料分析的核心，透過MapReduce的平行化架構可以大幅增加巨量資料分析的效率。本論文使用派翠網路針對MapReduce做視覺化建模，並驗證此模型滿足Reachability性質，再提出一個實際的巨量資料分析系統來驗證此模型的可行性，詳細描述了MapReduce平行化的內部細節，並指出在系統開發的過程中可能會犯下的錯誤，再以派翠網路模型提出錯誤預防機制，避免系統開發者與系統使用者犯錯，進而使系統開發能更有效率。

Technological advances have significantly increased the amount of corporate data available, which has created a wide range of business opportunities related to big data and cloud computing. Hadoop is a popular programming framework used for the setup of cloud computing systems. The MapReduce framework forms the core of the Hadoop program for parallel computing and its parallel framework can greatly increase the efficiency of big data analysis. This study used Petri nets to create a visual model of the MapReduce framework and verify its reachability. We present an actual big data analysis system to demonstrate the feasibility of the model, describe the internal procedures of the MapReduce framework in detail, list common errors during the system development process and propose error prevention mechanisms using the Petri net model in order to increase efficiency in the system development.

Acknowledgements I
Abstract (Chinese) II
Abstract (English) III
Table of Contents V
List of Figures VII
List of Tables VIII
Chapter 1 Introduction 1
1-1 Motivation and Purposes 1
1-2 Thesis Organization 3
Chapter 2 Literature Review 4
2-1 Framework of Hadoop MapReduce 4
2-2 Petri Nets 6
2-3 Properties of Petri Nets 8
2-3-1 Liveness 8
2-3-2 Reachability 9
2-3-3 Incidence Matrix 9
2-4 Petri Net Model of MapReduce Framework 10
2-5 Reachability Verification Using Petri Net Model 12
2-6 Computation Tree Logic (CTL) 16
2-7 Linear Temporal Logic (LTL) 17
2-8 Tool Introduction – WoPeD 18
Chapter 3 The Proposed Approach 20
3-1 Parallel MapReduce System for Big-Data Analysis 20
3-2 Detailed Procedures for Parallel MapReduce Framework 23
3-3 Inclusion of Check Procedures in the System 26
3-3-1 File Checker 26
3-3-2 Rule Checker 27
3-4 Big Data Analysis System by Inclusion of Checking Mechanisms 29
Chapter 4 Main Results and Analysis 33
4-1 Common Errors Detection 33
4-1-1 File Error Detection 33
4-1-2 Rule Error Detection 35
4-1-3 <Key, Value> pairs Error Detection 37
4-2 Comparison of the Proposed Approach with Other Methods 39
4-3 Property Analysis 41
4-3-1 Error Resolution 41
4-3-2 Reachability Analysis 42
Chapter 5 Conclusion and Future Work 43
References 44
Appendix – A 47
Software Tool : WoPeD 47
Appendix – B 50
Paper Acceptance Notification 50
Publication 51

[1]Tom White, Hadoop: The Definitive Guide, O’Reilly Media, 2009.
[2]Apache Hadoop. http://hadoop.apache.org/
[3]J. Dean and S. “Ghemawat, Mapreduce: Simplified data processing on large clusters.” , OSDI’04, pp. 137-150.
[4]N. Q. Wu and M. C. Zhou, System Modeling and Control with Resource-Oriented Petri Nets, CRC Press, New York, 2010.
[5]T. Murata, “Petri nets: properties, analysis, and applications,” Proc. IEEE, vol. 77, no. 4, pp. 541–580, Apr. 1989.
[6]A. Negahban and J. S. Smith, “Simulation for manufacturing system design and operation: literature review and analysis,” Journal of Manufacturing Systems, vol. 33, no. 2, pp. 241–261, Apr. 2014.
[7]P. C. Xiong, Y. S. Fan, and M. C. Zhou, “A Petri net approach to analysis and composition of Web services,” IEEE Transactions on System, Man, and Cybernetics—Part A: Systems and Humans, vol. 40, no.2, Mar. 2010.
[8]Y. Ru and C. N. Hadjicostis, “Bounds on the number of markings consistent with label observations in Petri nets,” IEEE Trans. Autom. Sci. Eng., vol. 6, no. 2, pp. 334–344, Apr. 2009.
[9]J. Rosell, “Assembly and task planning using Petri nets: A survey,” J. Eng. Manuf., vol. 218, no. 8, pp. 987–994, Aug. 2004.
[10]L. Li, Y. Ru, and C. N. Hadjicostis, “Least-cost firing sequence estimation in labeled Petri nets,” Proc. 45th IEEE Int. Conf. Decision and Control, pp. 416–421, Dec. 2006.
[11]Kala Karun. A, and Chitharanjan. K, “A review on Hadoop – HDFS infrastructure extensions,” 2013 IEEE Conference on Information and Communication Technologies (ICT 2013)
[12]Thomas Freytag, Martin Sänger, “WoPeD – An educational tool for workflow nets,” Proceedings of the BPM Demo Sessions, Eindhoven, pp. 31-35, September 2014.
[13]Matteo Camilli, Carlo Bellettini, Lorenzo Capra, Mattia Monga, “CTL model checking in the cloud using MapReduce,” Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 333-340, September 2014.
[14]Sylvain Hallé* and Maxime Soucy-Boivin, “MapReduce for parallel trace validation of LTL properties,” Journal of Cloud Computing:Advances, Systems and Applications, April 2015.
[15]Naldurg P, Sen K, Thati P, “A temporal logic based framework for intrusion detection. “ FORTE, Volume 3235 of Lecture Notes in Computer Science. pp 359–376, 2004.
[16]Madhavan Mukund , “Linear-time temporal logic and Büchi automata,” SPIC Mathematical Institute, 1996.
[17]A. Bell and B. R. Haverkort, “Sequential and distributed model checking of Petri nets,” International Journal on Software Tools for Technology Transfer, vol. 7, no. 1, pp. 43–60, 2005.
[18]M. Camilli, “Petri nets state space analysis in the cloud,” Proceedings of the 2012 International Conference on Software Engineering, pp. 1638–1640, 2012.
[19]F. Guo, G. Wei, M. Deng, and W. Shi, “CTL model checking algorithm using MapReduce,” Emerging Tech. for Inf. Syst. Computing, and Management, LNEE, vol. 236, pp. 341–348, 2013.
[20]Neil J. Gunther, Paul Puglia, and Kristofer Tomasette, “Hadoop Superlinear Scalability, ” Communications of the Acm, vol. 58, pp. 46-55, 2014.