MooseFS is verified formally
![Modeling and Verifying MooseFS in CSP post_thumbnail](https://moosefs.com/wp-content/uploads/2018/08/Modeling-and-Verifying-MooseFS-in-CSP-1024x653.png)
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
![MooseFS is Verified Formally; Source: https://github.com/AKKID/MooseFSCSPModel MooseFS is Verified Formally; Source: https://github.com/AKKID/MooseFSCSPModel](https://moosefs.com/wp-content/uploads/2018/08/MooseFS-is-Verified-Formally.png)
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.