Bit-packing and Hashing Evaluation in Explicit-state Model Checking

MCSTA is a model checking tool for models written in the Modest language. It can be used to formally verify certain properties of a model. During model checking a model’s state space needs to be (exhaustively) explored which takes a significant amount of time and memory – depending on model complexity. This research evaluates the impact of bit-packing state member variables by examining the execution time and memory consumption. We find that in all cases there is a decrease in memory usage, and in most cases a minor decrease in execution time. Furthermore, we propose an algorithm for selective field unpacking, to improve the performance of bit-packing, whilst maintaining near-optimal state sizes. Lastly, we evaluate the current hash function used in state space exploration based on hash-table bucket lengths, and find it to be performing adequately with little room for improvement.