Systematic API Testing Through Model Checking and Executable Contracts
This work addresses the test-oracle problem and stateful call sequence generation for API-based systems, offering a novel approach to improve testing effectiveness, though it is incremental in combining existing techniques like model checking with new contract specifications.
The paper tackles the problem of limited behavioral semantics in automated black-box API testing by introducing IcePick, a framework that uses model checking to achieve systematic state-space coverage, and Glacier, a contract language for automated behavioral verification, resulting in complete state coverage and fault detection in multi-operation interactions on benchmark systems.
Automated black-box testing of APIs typically relies on interface specifications that define available operations and data schemas, but offer limited or no behavioural semantics. This semantic gap amplifies the test-oracle problem and limits the generation of effective, stateful call sequences. We introduce IcePick, a framework that achieves systematic state-space coverage for API testing by leveraging model checking. IcePick uses TLA+ to formally model API state evolution, employs the TLC model checker to exhaustively explore reachable states, and generates test sequences that provably cover the behavioural model. To mitigate state-space explosion and improve sequence extraction, we introduce a coverage-guided breadth-first traversal of the TLC state-space graph. To address oracle limitations beyond HTTP status codes, we propose Glacier, a first-order logic contract language that enriches API specifications with executable semantic contracts, enabling automated behavioural verification during test execution. We evaluate IcePick on EvoMaster Benchmark systems, demonstrating that model-checking-guided exploration achieves complete state coverage and reveals faults in multi-operation interactions. We also analyse scalability to characterise practical limits and applicability requirements. Overall, IcePick provides reproducible test suites with strong coverage guarantees for critical API-based systems.