This post expolores, how to state space explosion manifests itself in formal models created by Sbuilder -tool, and how state space explosion can be controlled by limiting cardinality of domain sets in application data model.
NOTICE: mpashkovskiy has implemented Truffle tests for the Bank contract in https://github.com/mpashkovskiy/ethereum-bank-tests. These tests identified several issues in this post:
- missing payable modifiers
- false positive in Run 3 for setup3 – Find 2nd Bug (because environment model in sbuilder-eth allows using contract address as a message sender in a way which is not possible on EVM)
TODO: fix sbuilder-eth model and this blog post based on the findings in https://github.com/mpashkovskiy/ethereum-bank-tests.
This post uses a simple 10 line Solidity contract containing two (subtle) “bugs” (=violations of correctness promise), and a demonstrates, how to use invariants in Sbuilder to find these violations.
This blog entry uses a very contrived example to demonstrate, how to include manually crafted TLA+ snippets into a formal model created by SBuilder. The main purpose is to 1) show, how to bind TLA code with Solidity interfaces, 2) understand TLA -files generated in Sbuilder translation, and 3) explain, how Sbuilder “possibility” operator relates to model checking formal model correctness. A more realistic example of using manual TLA+ to specify is given in another post.
Sbuilder possibility operators may generate traces, which demonstrate that behaviour given by the operator is present in the model checking state space. An API trace is a sequence of steps, where a step includes the state of the formal model before the API call, interface operation called and its parameters bindings, and the state of formal model after the API call. This post shows to how to extend rendering of formal model API traces.