On the design and analysis of protocols for Personal Health Record storage on Personal Data Server devices

We need formal assurance of data availability when information is stored in PDS overlays. Thus, data must be replicated at multiple PDSs. We propose a data replication protocol that ensures that the PHRs for each user have replicas in the PDS overlay. It is crucial to ensure correctness of the data replication protocol. Consequently, we formalize the protocol using the Unified Modeling Language (UML) and specify a number of desirable properties. We need to provide formal assurance of these properties in an automated manner. We demonstrate how the UML model can be transformed into Alloy using the UML-to-Alloy transformations. This obviates the need for the protocol designer to know Alloy. The analysis uncovers a significant error in the protocol. Uncovering such errors help refine the protocol and ensures its correctness before deployment.