As described in the benchmark description, only the ReadFile message has a parameter called file, which can take on integer values in the range from 256 up to (and including) 511. Actually, each of these numbers has to be considered separately in the inference process, which would require a lot of time and memory space. By taking a closer look at the informal specification of the passport, we discovered that different files should be treated in the same way by the SUT. As one can see in Figure 1, files 257 and 258 should be readable after a BAC, 259 after a BAC followed by an EAC and the rest of the files should never be readable. Using this a priori knowledge about the passport, we can divide the values into three disjoint equivalence classes, which are:
In the abstraction mapping an abstract value is translated to a concrete one by randomly choosing an element within the corresponding equivalence class. If the numbers are partitioned incorrectly, then there are two values in the same class that produce a different response, which will give an error message.
