Introduce Simple ‘Specification Driven Development’ Demo and Point Out Improvements

This post introduces Simple “Specification Driven Development” Demo as a way to adapt Formal Methods to application development, also for existing applications. Benefits can be gained immediately in Test Management of System Tests, when using formal model to generate API traces, which are mapped as unit tests on existing application, and the aggregate result of individual unit tests interpreted as an execution of a “virtual” system test – easier to that managing the system test as single unit.

An analysis section identifies several less than optimal development architecture arrangement in the demo, and points out needs for improvements.



Specification Driven Development

This post argues that Application Management should use a design model, a representation describing aspects of a system that is not easily, or sufficiently, captured through implementation, in managing on-line openness in IT. The post introduces development architecture and specification driven process resulting to better systems, ease in system development management, ease in system test management, and generally allowing better control of IT development, and explains, how to keep design model and implementation in sync, and how scaling up of the approach is achieved.


Simple Bank Example

NOTICE: mpashkovskiy has implemented Truffle tests for the Bank contract in These tests identified several issues in this post:

TODO: fix sbuilder-eth model and this blog post based on the findings in

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.


Demonstrate Sbuilder Translation Results

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.


API Trace Rendering Extension Point

This post presents how API traces, generated for sbuilder formal models, can be inspected, and how the output can be modified using api-call-init extension point of tla-trace-filter -tool.

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.