Practical example: how to formally verify "file name" implementation from a spec?

Question

Say you have an OS-independent specification for file names. The file names are case sensitive, and let's say can't be more than 200 characters, and can't have : or / in the name.

Now say you want to implement this specification in C on different operating systems (different versions of linux and darwin, not windows for now).

Let's say for argument's sake, it turns out on some operating system (operating system "A"), that you also can't use | in the file name. Well, you didn't capture this in your spec initially.

The question is, how do you figure this out before running into this case? In circuits (from my understanding), you can use "model checking" to automatically explore all possible states of the system, to figure out edge cases your spec doesn't handle. That makes sense for relatively simple state machines like logic circuits. But what about this case with file names?

How would you generate file names, and try to save the file on that operating system, so it can discover these implementation errors, without having to generate every possible string up to 200 characters in length?

How do you verify that the implementation of the spec on operating system "A" is valid? The model checker would have to somehow randomly construct a file name using the | character, and then hit an error. Or maybe I am misunderstanding model checking, and what this really is is automatic testing.

What I'm wondering is, how do you account for these types of cases in advance using formal methods? What are the general techniques or topics to start looking into?

Answer 1

In general, the technique used is known as "fuzzing". Not all errors are equally likely. Let's consider two hypothetical errors:

1. System A incorrectly rejects a filename if it contains an | anywhere.
2. System A incorrectly rejects a filename if it contains a prime number of b characters.

Errors of the second type are much, much rarer, but this is not explained by Computer Science. It's a result from how humans construct software. Fuzzing tries to focus on typical human bugs. In this case, we can predict the following types of errors are more likely:

1. Very short paths and very long paths may have boundary errors.
2. Errors near the begin or end of the path are more common than errors at the end
3. Many characters can be organized into classes which are treated identically, such as lowercase characters. All characters in this class are treated equally, so whether a filename is valid does not depend on a substitution within the class.
4. Some characters are a priori known to be problematic and each should be treated as a class on its own. (Examples: <>/\&:")
5. Duplicating characters is more likely to cause bugs the closer they're together.

Fuzzing aims to generate a smaller set of strings by omitting irrelevant variations. We obviously generate an initial set of testcases of all possible lengths (1-200). This checks rule 1. We then expand this set by varying a few characters near both ends. We might try varying the 150th character of the 170 character testcase, but we won't bother with all 254 variations. Nor will we add a variation in the 151th character.

Answer 2

For the concrete case of a specification of a regular language, there is the Java String Analyzer which roughly is able to compute a finite state automaton (i.e. regular expression) of the set of strings accepted by a Java method, using various techniques in static analysis.

While the paper deals directly with the set of strings generated by a piece of Java code, I believe the same techniques apply to the problem of checking whether a piece of code accepts the right inputs.