M in FISC is the state transition graph of a file system (e.g., ext3) inside the operating system kernel. A state consists of the kernel heap and data, the disk, and an abstract model of the file system data. A transition is either a test driver operation (regular operations on a  file system, such as creating, removing, or renaming files) or file system specific kernel thread execution (such as flushing blocks to disk). The initial state of this model is a state with an empty, formatted disk.

There is more than one formula Φ in FISC – every property that is checked by FISC is a Φ. FISC does some generic checks to ensure there is no deadlock, no null pointer dereference, unbalanced function call pairs, memory leaks, or silent failures. In addition to these properties, FISC performs a few consistency checks: First, it ensures that what is visible to the user after all performed transitions conforms to what it should be. This property is a kind of black-box property. Other consistency properties are: recoverable disk write ordering, changed buffers are marked dirty, and buffer consistency. The two latter properties require intimate knowledge of file system design.

M in MODIST is the state transition graph of a distributed system. A state is an instantaneous snapshot of the target system. A transition is any possible action that changes the state: it might be a regular system action, a failure, or a timer fired from another component. The initial state in this graph is specified by user-provided configuration files.

Similar to FISC, every property which is checked in MODIST is a Φ. The first property is the absence of regular system crashes, such as segmentation faults or program aborts. Second – no deadlocks. Third – no infinite loops. MODIST can also check user-provided assertions, and it provides a general mechanism for defining such properties.