Skip to main content
Erschienen in: Mobile Networks and Applications 2/2017

16.02.2017

Modeling and Verifying HDFS Using Process Algebra

verfasst von: Wanling Xie, Huibiao Zhu, Xi Wu, Shuangqing Xiang, Jian Guo, Phan Cong Vinh

Erschienen in: Mobile Networks and Applications | Ausgabe 2/2017

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Hadoop Distributed File System (HDFS) is a high fault-tolerant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Since HDFS is widely used, analysis on it in a formal framework is of great significance. In this paper, we use Communicating Sequential Processes (CSP) to model and analyze HDFS. We mainly focus on the dominant parts which include reading files and writing files in HDFS and formalize them in detail. Moreover, we also model the heartbeat mechanism. Finally, we use the model checker Process Analysis Toolkit (PAT) to simulate the model constructed and verify whether it caters for the specification and some important properties, which include Deadlock-freeness, Minimal Distance Scheme, Mutual Exclusion, Write-Once Scheme and Robustness.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Weitere Produktempfehlungen anzeigen
Literatur
1.
Zurück zum Zitat Azzedin F (2013) Towards a scalable HDFS architecture 2013 International conference on collaboration technologies and systems, CTS 2013, San Diego, CA, USA, May 20-24, 2013, pp 155–161. doi:10.1109/CTS.2013.6567222 Azzedin F (2013) Towards a scalable HDFS architecture 2013 International conference on collaboration technologies and systems, CTS 2013, San Diego, CA, USA, May 20-24, 2013, pp 155–161. doi:10.​1109/​CTS.​2013.​6567222
3.
4.
Zurück zum Zitat Buyya R, Yeo CS, Venugopal S, Broberg J, Brandic I (2009) Cloud computing and emerging IT platforms: Vision, hype, and reality for delivering computing as the 5th utility. Future Generation Comp Syst 25(6):599–616. doi:10.1016/j.future.2008.12.001. Buyya R, Yeo CS, Venugopal S, Broberg J, Brandic I (2009) Cloud computing and emerging IT platforms: Vision, hype, and reality for delivering computing as the 5th utility. Future Generation Comp Syst 25(6):599–616. doi:10.​1016/​j.​future.​2008.​12.​001.
6.
Zurück zum Zitat Dong B, Zheng Q, Tian F, Chao K, Ma R, Anane R (2012) An optimized approach for storing and accessing small files on cloud storage. J Network and Computer Applications 35(6):1847-1862. doi:10.1016/j.jnca.2012.07.009. Dong B, Zheng Q, Tian F, Chao K, Ma R, Anane R (2012) An optimized approach for storing and accessing small files on cloud storage. J Network and Computer Applications 35(6):1847-1862. doi:10.​1016/​j.​jnca.​2012.​07.​009.
7.
Zurück zum Zitat Dong B, Zheng Q, Tian F, Chao K, Godwin N, Ma T, Xu H (2014) Performance models and dynamic characteristics analysis for HDFS write and read operations: A systematic view. J Syst Softw 93:132–151. doi:10.1016/j.jss.2014.02.038. Dong B, Zheng Q, Tian F, Chao K, Godwin N, Ma T, Xu H (2014) Performance models and dynamic characteristics analysis for HDFS write and read operations: A systematic view. J Syst Softw 93:132–151. doi:10.​1016/​j.​jss.​2014.​02.​038.
8.
Zurück zum Zitat Ghemawat S, Gobioff H, Leung S (2003) The google file system Proceedings of the 19th ACM symposium on operating systems principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19-22, 2003, pp 29–43. doi:10.1145/945445.945450 Ghemawat S, Gobioff H, Leung S (2003) The google file system Proceedings of the 19th ACM symposium on operating systems principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19-22, 2003, pp 29–43. doi:10.​1145/​945445.​945450
9.
Zurück zum Zitat Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall International in Computer Science Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall International in Computer Science
10.
Zurück zum Zitat Liu Y, Sun J, Dong JS (2010) Analyzing hierarchical complex real-time systems. In: Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November 7-11, 2010, pp 365-366. doi:10.1145/1882291.1882350 Liu Y, Sun J, Dong JS (2010) Analyzing hierarchical complex real-time systems. In: Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November 7-11, 2010, pp 365-366. doi:10.​1145/​1882291.​1882350
12.
14.
Zurück zum Zitat Milner R (1980) A Calculus of Communicating Systems, vol 92, Springer. Lecture Notes in Computer Science Milner R (1980) A Calculus of Communicating Systems, vol 92, Springer. Lecture Notes in Computer Science
15.
Zurück zum Zitat Roscoe AW (1997) The Theory and Practice of Concurrency. Prentice Hall International in Computer Science Roscoe AW (1997) The Theory and Practice of Concurrency. Prentice Hall International in Computer Science
16.
Zurück zum Zitat Roscoe AW (2007) Understanding Concurrent Systems, Springer Verlag Roscoe AW (2007) Understanding Concurrent Systems, Springer Verlag
18.
Zurück zum Zitat Shafer J, Rixner S, Cox AL (2010) The hadoop distributed filesystem: Balancing portability and performance. In: IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS 2010, www.ispass.org, 28-30 March 2010, White Plains, NY, USA, pp 122–133. doi:10.1109/ISPASS.2010.5452045 Shafer J, Rixner S, Cox AL (2010) The hadoop distributed filesystem: Balancing portability and performance. In: IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS 2010, www.ispass.org, 28-30 March 2010, White Plains, NY, USA, pp 122–133. doi:10.​1109/​ISPASS.​2010.​5452045
19.
Zurück zum Zitat Shvachko K, Kuang H, Radia S, Chansler R (2010) The hadoop distributed file system. In: IEEE 26th symposium on mass storage systems and technologies, MSST 2012, Lake Tahoe, Nevada, USA, May 3-7, 2010, pp 1–10 Shvachko K, Kuang H, Radia S, Chansler R (2010) The hadoop distributed file system. In: IEEE 26th symposium on mass storage systems and technologies, MSST 2012, Lake Tahoe, Nevada, USA, May 3-7, 2010, pp 1–10
20.
Zurück zum Zitat Si Y, Sun J, Liu Y, Dong JS, Pang J, Zhang SJ, Yang X (2014) Model checking with fairness assumptions using PAT. Frontiers of Computer Science 8(1):1–16. doi:10.1007/s11704-013-3091-5. Si Y, Sun J, Liu Y, Dong JS, Pang J, Zhang SJ, Yang X (2014) Model checking with fairness assumptions using PAT. Frontiers of Computer Science 8(1):1–16. doi:10.​1007/​s11704-013-3091-5.
21.
Zurück zum Zitat Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: Introducing a process analysis toolkit. In: Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation, 3rd International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15, 2008, pp 307–322. doi:10.1007/978-3-540-88479-8_22 Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: Introducing a process analysis toolkit. In: Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation, 3rd International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15, 2008, pp 307–322. doi:10.​1007/​978-3-540-88479-8_​22
22.
Zurück zum Zitat Sun J, Liu Y, Dong JS, Pang J (2009) Pat: Towards flexible verification under fairness. In: Proceedings of the 21th international conference on computer aided verification (CAV’09), Springer, lecture notes in computer science, vol 5643, pp 709–714. doi:10.1007/978-3-642-02658-4_59 Sun J, Liu Y, Dong JS, Pang J (2009) Pat: Towards flexible verification under fairness. In: Proceedings of the 21th international conference on computer aided verification (CAV’09), Springer, lecture notes in computer science, vol 5643, pp 709–714. doi:10.​1007/​978-3-642-02658-4_​59
23.
Zurück zum Zitat Sun J, Liu Y, Song S, Dong JS, Li X (2011) PRTS: An approach for model checking probabilistic real-time hierarchical systems. In: Proceedings of the Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011, pp 147-162. doi:10.1007/978-3-642-24559-6_12 Sun J, Liu Y, Song S, Dong JS, Li X (2011) PRTS: An approach for model checking probabilistic real-time hierarchical systems. In: Proceedings of the Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011, pp 147-162. doi:10.​1007/​978-3-642-24559-6_​12
24.
Zurück zum Zitat Sun J, Liu Y, Dong J S, Liu Y, Shi L, André É (2013) Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3. doi:10.1145/2430536.2430537. Sun J, Liu Y, Dong J S, Liu Y, Shi L, André É (2013) Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3. doi:10.​1145/​2430536.​2430537.
25.
26.
Zurück zum Zitat Wang F, Qiu J, Yang J, Dong B, Li X H, Li Y (2009) Hadoop high availability through metadata replication Proceedings of the First International CIKM Workshop on Cloud Data Management, CloudDb 2009, Hong Kong, China, November 2, 2009, pp 37-44. doi:10.1145/1651263.1651271 Wang F, Qiu J, Yang J, Dong B, Li X H, Li Y (2009) Hadoop high availability through metadata replication Proceedings of the First International CIKM Workshop on Cloud Data Management, CloudDb 2009, Hong Kong, China, November 2, 2009, pp 37-44. doi:10.​1145/​1651263.​1651271
27.
Zurück zum Zitat Wu X, Zhu H, Zhao Y, Wang Z, Liu S (2013) Modeling and verifying the ariadne protocol using process algebra. Comput Sci Inf Syst 10(1):393-421. doi:10.2298/CSIS120601009W. Wu X, Zhu H, Zhao Y, Wang Z, Liu S (2013) Modeling and verifying the ariadne protocol using process algebra. Comput Sci Inf Syst 10(1):393-421. doi:10.​2298/​CSIS120601009W.
28.
Metadaten
Titel
Modeling and Verifying HDFS Using Process Algebra
verfasst von
Wanling Xie
Huibiao Zhu
Xi Wu
Shuangqing Xiang
Jian Guo
Phan Cong Vinh
Publikationsdatum
16.02.2017
Verlag
Springer US
Erschienen in
Mobile Networks and Applications / Ausgabe 2/2017
Print ISSN: 1383-469X
Elektronische ISSN: 1572-8153
DOI
https://doi.org/10.1007/s11036-017-0812-2

Weitere Artikel der Ausgabe 2/2017

Mobile Networks and Applications 2/2017 Zur Ausgabe

Neuer Inhalt