Systematic API Testing Through Model Checking and Executable Contracts

TL;DR

IcePick is a framework that uses model checking and executable contracts to systematically generate API test sequences with strong coverage guarantees, addressing limitations of traditional black-box testing.

Contribution

It introduces IcePick, combining TLA+ modeling, TLC model checking, and a new contract language Glacier to improve API testing coverage and behavioral verification.

Findings

Achieves complete state coverage in API testing scenarios.

Reveals faults in multi-operation API interactions.

Demonstrates scalability and practical applicability on benchmark systems.

Abstract

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.