Towards Model-based Verification of a Key-Value Storage Engine

This post details the application of model-based verification to the WiredTiger storage engine, building upon the previous work on specifying MongoDB's distributed transactions protocol. It describes how a modified TLC model checker is used to generate a large suite of API call test cases (87,143 tests for a small model) by computing path coverings in the state graph of the storage component specification. This enables automated checking of conformance between the WiredTiger implementation and the abstract storage specification, which serves as the contract for the distributed transactions protocol. The post highlights the modularity of the specification and the ability to automatically check interface boundaries.