1 Background Information

1.1 Read an article “How Amazon uses formal methods”

post summarizes experiences Amazon has gained, when using TLA+ specification tools, and discusses, what is needed to start using formal methods in business IT development context

1.2 Emerging API Ecosystems

blog entry argues that managing on-line openness has become more important for businesses with the emergence of API ecosystems, and, in the future, it will be even more important as blockchain technologies mature. To help in managing on-line openness this post suggests modeling API ecosystem.

It is the first of two blog entries updating roadmap v1 in sbuilder vision.

1.3 A Tool To Generate Runnable Specification Models in TLA+ language

post introduces Sbuilder (aka Specification Builder) -tool. Sbuilder generates runnable specification models in TLA+ language for business IT system. Specification model can be verified using TLA+Tools, and parts of it can be presented as implementation blueprints to developers.

1.4 Announcing Support for Ethereum

post announces sbuilder-ethereum, a tla-sbuilder plugin, to translate Ethereum implementations in Solidity language into in TLA+ language formal models to be model checked using TLA+ Tools.

1.5 Specification Driven Development

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.

1.6 Presentations

Helsinki Ethereum Meetup 11th Nov 2017

post links to slides for a presentation held on the 8th Nov 2017 in Ethererum Meetup Helsinki.

Helsinki Ethereum Meetup 8th March 2017

post contains slides for a presentation on Sbuilder model checking performance, held on the 8th March 2017 in Ethererum Meetup Helsinki.

Helsinki Ethereum Meetup 14th Dec 2016

post contains slides for a presentation held on the 14th Dec 2016 in Ethererum Meetup Helsinki.

2 Roadmap

2.1 Sbuilder Roadmap v3 – aka Introduce Simple ‘Specification Driven Development’ Demo and Point Out Improvements

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.

2.2 Sbuilder Roadmap v2

post gives a short introduction to sbuilder -tool, and proposes changes (roadmap v2) in the tool for better support to reason on correctness of API ecosystem implementations.

It is the second of two blog entries updating roadmap v1 in sbuilder vision.

2.3 Sbuilder Roadmap v1

post argues that instead of deploying Sbuilder to support an upfront design step, it should be embedded into a framework. The post entry describes enhancements required in the current 0.2.3 version, and identifies a need for a proof of concept to better understand the feasibility of the proposal.

3 User’s Guide

3.1 SBuilder User’s Guide Blog Series

A series of posts comprising a User’s Guide for sbuilder-eth plugin in SBuilder tool:

  • Truffle install: documents steps to install Truffle Ethereum development environment to Node-js.
  • Sbuilder install: shows steps to install sbuilder-eth GEM to Truffle Ethereum development environment. After installation a minimal configuration is used to validate that the installation was successful.
  • Managing state space generation in Sbuilder: expolore, 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.
  • Simple Bank contract: use 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.
  • Sbuilder generated correctness criteria: demonstrates using Sbuilder generated correctness criteria. The criteria presented include ensuring correctness of 1) contract function return values, 2) contract type, and 3) account balances on blockchain.
  • Demonstrate Sbuilder Translation Results (Wallet-1): use 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.
  • Translate Solidity Automatically (Wallet-2): explains how to integrate manually crafted and automatically translated TLA+ snippets to work together in a Sbuilder formal model.
  • API Trace Extension Point (Wallet-3): 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.

3.2 Using Sbuilder to Model Business IT Systems

post uses an example to demonstrate, how business IT system modeling can be supported using Sbuilder -tool. The example mimics a simple Pet Store application with two services. One of the services is used to manage pets, and the other one to manage tags.

3.3 Check Correctness of Ethereum Contracts for Re-Entract Attack

post presents an example using Ethereum Solidity language withdrawal pattern to demonstrate, how tla-sbuilder with sbuilder-ethererum plugin can be used to check for implementation correctness.

4 Developer’s Guide

4.1 Benchmarking Sbuilder

post examines TLA+tools model checker performance, as a number of states processed per second, when model checking formal models generated by Sbuilder. It finds the performance to be CPU bound, but scalable to match real world applications.

The blog entry demonstrates, how Setups in Sbuilder can be used to manage state space explosion, and associates setups with Use Case Slices to make the idea of managing state space size more comprehensible for developers. Ideally, a Use Case Slice, identified in development, is configured as an Sbuidler Setup and added into a repository for Regression Verification. The objective is to increase confidence in application correctness, and to make QA more efficient with faster feed back because a formal model

  • can be executed without the need to have it installed on real production environment, and
  • the model checker can effectively check all possible executions in the formal model.

4.2 Running Sbuilder Benchmarks

post documents, how Sbuilder Benchmarks were run.

4.3 Tla-sbuilder API loader Plugin Developers’s Guide

post gives an overview of Sbuilder framework, and information, how to create an API loader plugin, like Salesforce API loader, for tla-sbuilder -tool.

5 Deprecated

5.1 Using Sbuilder to Model a Salesforce Application

post explains, how to build a runnable specification model for a Salesforce application in sbuilder-demo GIT repository using tla-sbuilder -tool. The example uses Salesforce API plugin to extract interface specification from Salesforce API metadata.

5.2 Tla-sbuilder Salesforce API plugin User’s Guide

post demonstrates how to use Salesforce API plugin for tla-sbuilder -tool to access Salesforce API metadata to model an interfaces in a example application.