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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Andreozzi, S., Sgaravatto, M., Vistoli, M.C.: Sharing a Conceptual Model of Grid Resources and Services. CoRR, cs.DC/0306111 (2003)
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)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
CPN Tools Homepage, http://www.cpntools.org
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)
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)
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)
Badino, P., et al.: The Storage Resource Manager Interface Specification v2.2. Technical report, Lawrence Berkeley National Laboratory (2009)
Andreozzi, S., et al.: GLUE Schema Specification version 1.3. Technical report, INFN - Istituto Nazionale di Fisica Nucleare, Italy (January 2007)
Industrial Use of CPNs, http://www.cs.au.dk/CPnets/intro/example/indu.html
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)
Jensen, K., Kristensen, L.M.: Coloured Petri Nets – Modelling and Validation of Concurrent Systems. Springer, Heidelberg (2009)
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)
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)
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)
Chelonia CPN Model, http://www.hib.no/ansatte/lmkr/cpnchelonia.xml
Nagy, Z., Nilsen, J., Toor, S.Z.: Chelonia - Self-healing Distributed Storage System – NorduGrid Technical Report 17 (2010), http://www.knowarc.eu/chelonia/
Nagy, Z., Nilsen, J., Toor, S.Z.: Chelonia - Self-healing Distributed Storage System - Documentation of the ARC Storage System. Technical report, NORDUGRID (February 2010)
Reisig, W.: Petri Nets. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer, Heidelberg (1985)
Ullman, J.D.: Elements of ML Programming. Prentice-Hall, Englewood Cliffs (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Taktak, S., Kristensen, L.M. (2011). Formal Modelling and Initial Validation of the Chelonia Distributed Storage System. In: Riekki, J., Ylianttila, M., Guo, M. (eds) Advances in Grid and Pervasive Computing. GPC 2011. Lecture Notes in Computer Science, vol 6646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20754-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-20754-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20753-2
Online ISBN: 978-3-642-20754-9
eBook Packages: Computer ScienceComputer Science (R0)