Advertisement

Formal Modelling and Initial Validation of the Chelonia Distributed Storage System

  • Sami Taktak
  • Lars M. Kristensen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6646)

Abstract

A storage system with file replication is an important element in supporting reliable and fault tolerant file access in many grid computing systems. The Chelonia distributed storage system is being developed in the context of the NorduGrid project. It provides transparent access to replicated files stored on a heterogeneous collection of storage nodes with files being organised in a global name space. Our contribution is to develop a formal specification of the operations supported by the Chelonia system using the Coloured Petri Nets modelling language with the aim of verifying functional correctness. An important contribution of our formal modelling approach is to abstract from the concrete data stored on the storage nodes within the system. This caters for verification of the storage operations using finite-state model checking techniques.

Keywords

Model Check Storage Node Port Place Model Check Technique Substitution Transition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Andreozzi, S., Sgaravatto, M., Vistoli, M.C.: Sharing a Conceptual Model of Grid Resources and Services. CoRR, cs.DC/0306111 (2003)Google Scholar
  2. 2.
    Bratosin, C., van der Aalst, W.M.P., Sidorova, N.: Modeling Grid Workflows with Colored Petri Nets. In: Proc. Workshop on the Practical Use of Coloured Petri Nets and CPN Tools, pp. 67–86. Aarhus University - DAIMI-PB 584 (2007)Google Scholar
  3. 3.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  4. 4.
    CPN Tools Homepage, http://www.cpntools.org
  5. 5.
    Dalheimer, M., Pfreundt, F., Merz, P.: Formal Verification of a Grid Resource Allocation Protocol. In: Proc. of CCGRID 2008, pp. 332–339. IEEE, Los Alamitos (2008)Google Scholar
  6. 6.
    Domenici, A., Donno, F.: Static and Dynamic Data Models for the Storage Resource Manager v2.2. Journal of Grid Computing 7(1), 115–133 (2009)CrossRefGoogle Scholar
  7. 7.
    Li, B., et al.: A Formal Model for the Grid Security Infrastructure. In: Zhou, X., Su, S., Papazoglou, M.P., Orlowska, M.E., Jeffery, K. (eds.) WISE 2004. LNCS, vol. 3306, pp. 706–717. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Badino, P., et al.: The Storage Resource Manager Interface Specification v2.2. Technical report, Lawrence Berkeley National Laboratory (2009)Google Scholar
  9. 9.
    Andreozzi, S., et al.: GLUE Schema Specification version 1.3. Technical report, INFN - Istituto Nazionale di Fisica Nucleare, Italy (January 2007)Google Scholar
  10. 10.
  11. 11.
    Hlaoui, Y., Benayed, L.: Symbolic Model Checking Supporting Formal Verification of Grid Service Workflow Models Specified by UML Activity Diagrams. In: Proc. of NOTERE 2010, pp. 255–260. IEEE Computer Society, Los Alamitos (2010)Google Scholar
  12. 12.
    Jensen, K., Kristensen, L.M.: Coloured Petri Nets – Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009)CrossRefzbMATHGoogle Scholar
  13. 13.
    Lai, H.F.: Modeling Grid Workflow by Coloured Grid Service Net. In: Bellavista, P., Chang, R.-S., Chao, H.-C., Lin, S.-F., Sloot, P.M.A. (eds.) GPC 2010. LNCS, vol. 6104, pp. 204–213. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Manset, D., Verjus, H., McClatchey, R., Oquendo, F.: A Formal Architecture-Centric Model-Driven Approach for the Automatic Generation of Grid Applications. CoRR, abs/cs/0601118 (2006)Google Scholar
  15. 15.
    Mascheroni, M., Farina, F.: Nets Within Nets Paradigm and Grid Computing. In: Proc. of PNSE 2010, pp. 23–38. Universitat Hamburg - FBI-HH-B-294/10 (2010)Google Scholar
  16. 16.
  17. 17.
    Nagy, Z., Nilsen, J., Toor, S.Z.: Chelonia - Self-healing Distributed Storage System – NorduGrid Technical Report 17 (2010), http://www.knowarc.eu/chelonia/
  18. 18.
    Nagy, Z., Nilsen, J., Toor, S.Z.: Chelonia - Self-healing Distributed Storage System - Documentation of the ARC Storage System. Technical report, NORDUGRID (February 2010)Google Scholar
  19. 19.
    Reisig, W.: Petri Nets. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)CrossRefzbMATHGoogle Scholar
  20. 20.
    Ullman, J.D.: Elements of ML Programming. Prentice-Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Sami Taktak
    • 1
  • Lars M. Kristensen
    • 1
  1. 1.Department of Computer EngineeringBergen University CollegeNorway

Personalised recommendations