Model-Checking Support for File System Development