MooseFS Formally Verified
Researchers at East China Normal University used CSP modelling and the FDR model checker to formally verify MooseFS read/write operations — confirming deadlock freedom, mutual exclusion, divergence-free behaviour, and a correct backup scheme. Their findings were published at IEEE COMPSAC 2018.
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 independent scientists!
Full Paper Available
The full paper is available in the IEEE Xplore Digital Library.