Como sistema de información típico, un sistema de archivos en la nube permite el almacenamiento, recuperación y gestión de datos en servidores remotos o clusters de servidores. El diseño fiable de tales sistemas es crítico para garantizar la seguridad de los datos y la disponibilidad de los servicios. Sin embargo, diseñar sistemas correctos por construcción es un desafío debido a la complejidad y la concurrencia inherente en los sistemas de archivos en la nube. Además, los trabajos existentes sobre el análisis de sistemas de archivos en la nube a menudo se centran en sistemas específicos o carecen de modelado y verificación formales, lo que puede llevar a posibles fallos de diseño y vulnerabilidades de seguridad. Para abordar estos problemas, proponemos MSCFS-RP, que es un modelo de análisis formal basado en redes de Petri coloreadas. Aprovechando las fortalezas de las redes de Petri coloreadas en la representación de diversos tipos de información con fichas coloreadas y en la definición de reglas explícitas para interacciones concurrentes, nuestro modelo captura los procesos de escritura y lectura de clientes, metaservidores y clusters. Con un fuerte formalismo y soporte para la verificación utilizando CPN Tools, evaluamos rigurosamente propiedades clave como la consistencia de replicación bajo diversos escenarios. Los resultados demuestran que MSCFS-RP satisface estas propiedades, validando su efectividad y confiabilidad en la gestión de información dentro de los sistemas de almacenamiento en la nube.