MooseFS is verified formally
MooseFS is verified formally by researchers from East China Normal University. They used Communicating Sequential Process (CSP) to model and analyze MooseFS. The paper Modelling and Verifying MooseFS in CSP is published in 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC).
They focused mainly on reading and writing files and formalized them in detail. Then they used model checker Failures Divergence Refinement (FDR) to simulate the developed model and verify whether the model is consistent with the specification.
Verified properties:
- Deadlock freedom
- Divergence-free
- Mutual exclusion
- Backup scheme
They have constructed models for Master, Client, and Chunkservers modeled the read and write operations through CSP. They constructed and verified the specific models based on the four properties. The results showed their model satisfied all those properties, indicating MooseFS gets a strong robustness and is consistent with the specification. They plan to improve formal models by introducing component failures and time behaviors. They will also compare MooseFS with other distributed file systems and analyze their performance.
The whole MooseFS Team is very proud that high quality of MooseFS was confirmed by the independed scientists!
Full paper available
The full paper available in IEEE Xplore Digital Library: https://ieeexplore.ieee.org/document/8377667/
If you are ready to try MooseFS, go to Download page.