• What exactly is it that the model models? (What is the "essence" of a file system?)

  • What sorts of interleaving/concurrency does the model handle? What about two racing writes, can they interleave?

  • How is the equivalence partitioning and trace generation implemented?

  • Is it surprising that more bugs weren't found, particularly security bugs?

  • Why don't you test for concurrent/racy file system bugs?

  • How was the model constructed?

results matching ""

    No results matching ""